S (axiom)
Sdep.add [in add]
Sdep.cardinal [in cardinal]
Sdep.choose [in choose]
Sdep.choose_equal [in choose_equal]
Sdep.compare [in compare]
Sdep.diff [in diff]
Sdep.elements [in elements]
Sdep.empty [in empty]
Sdep.equal [in equal]
Sdep.eq_refl [in eq_refl]
Sdep.eq_sym [in eq_sym]
Sdep.eq_trans [in eq_trans]
Sdep.eq_In [in eq_In]
Sdep.exists_ [in exists_]
Sdep.filter [in filter]
Sdep.fold [in fold]
Sdep.for_all [in for_all]
Sdep.In [in In]
Sdep.inter [in inter]
Sdep.is_empty [in is_empty]
Sdep.lt [in lt]
Sdep.lt_not_eq [in lt_not_eq]
Sdep.lt_trans [in lt_trans]
Sdep.max_elt [in max_elt]
Sdep.mem [in mem]
Sdep.min_elt [in min_elt]
Sdep.partition [in partition]
Sdep.remove [in remove]
Sdep.singleton [in singleton]
Sdep.subset [in subset]
Sdep.t [in t]
Sdep.union [in union]
SetsOn.choose_spec3 [in choose_spec3]
SetsOn.compare_spec [in compare_spec]
SetsOn.elements_spec2 [in elements_spec2]
SetsOn.max_elt_spec3 [in max_elt_spec3]
SetsOn.max_elt_spec2 [in max_elt_spec2]
SetsOn.max_elt_spec1 [in max_elt_spec1]
SetsOn.min_elt_spec2 [in min_elt_spec2]
SetsOn.min_elt_spec3 [in min_elt_spec3]
SetsOn.min_elt_spec1 [in min_elt_spec1]
Sfun.choose_3 [in choose_3]
Sfun.compare [in compare]
Sfun.elements_3 [in elements_3]
Sfun.elements_3 [in elements_3]
Sfun.lt [in lt]
Sfun.lt_not_eq [in lt_not_eq]
Sfun.lt_trans [in lt_trans]
Sfun.max_elt [in max_elt]
Sfun.max_elt_1 [in max_elt_1]
Sfun.max_elt_3 [in max_elt_3]
Sfun.max_elt_2 [in max_elt_2]
Sfun.min_elt_3 [in min_elt_3]
Sfun.min_elt_2 [in min_elt_2]
Sfun.min_elt_1 [in min_elt_1]
Sfun.min_elt [in min_elt]
Sord.compare [in compare]
Sord.eq [in eq]
Sord.eq_refl [in eq_refl]
Sord.eq_1 [in eq_1]
Sord.eq_2 [in eq_2]
Sord.eq_sym [in eq_sym]
Sord.eq_trans [in eq_trans]
Sord.lt [in lt]
Sord.lt_not_eq [in lt_not_eq]
Sord.lt_trans [in lt_trans]
Sqrt.sqrt [in sqrt]
SWithLeibniz.eq_leibniz [in eq_leibniz]