MP (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Var0.TFunName.StP.MP)

module Dec : sig ... end

module FM : sig ... end

val coq_In_dec : St.elt -> St.t -> bool

val of_list : St.elt list -> St.t

val to_list : St.t -> St.elt list

val fold_rec : 
  (St.elt -> 'a1 -> 'a1) ->
  'a1 ->
  St.t ->
  (St.t -> __ -> 'a2) ->
  (St.elt -> 'a1 -> St.t -> St.t -> __ -> __ -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_bis : 
  (St.elt -> 'a1 -> 'a1) ->
  'a1 ->
  St.t ->
  (St.t -> St.t -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2 ->
  (St.elt -> 'a1 -> St.t -> __ -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_nodep : 
  (St.elt -> 'a1 -> 'a1) ->
  'a1 ->
  St.t ->
  'a2 ->
  (St.elt -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_weak : 
  (St.elt -> 'a1 -> 'a1) ->
  'a1 ->
  (St.t -> St.t -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2 ->
  (St.elt -> 'a1 -> St.t -> __ -> 'a2 -> 'a2) ->
  St.t ->
  'a2

val fold_rel : 
  (St.elt -> 'a1 -> 'a1) ->
  (St.elt -> 'a2 -> 'a2) ->
  'a1 ->
  'a2 ->
  St.t ->
  'a3 ->
  (St.elt -> 'a1 -> 'a2 -> __ -> 'a3 -> 'a3) ->
  'a3

val set_induction : 
  (St.t -> __ -> 'a1) ->
  (St.t -> St.t -> 'a1 -> St.elt -> __ -> __ -> 'a1) ->
  St.t ->
  'a1

val set_induction_bis : 
  (St.t -> St.t -> __ -> 'a1 -> 'a1) ->
  'a1 ->
  (St.elt -> St.t -> __ -> 'a1 -> 'a1) ->
  St.t ->
  'a1

val cardinal_inv_2 : St.t -> Datatypes.nat -> St.elt

val cardinal_inv_2b : St.t -> St.elt