MP (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Var0.SvExtra.SvP.MP)

module Dec : sig ... end

module FM : sig ... end

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

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

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

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

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

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

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

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

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

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

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

val cardinal_inv_2b : Sv.t -> Sv.elt