M (axiom)
MiniDecidableType.eq_dec [in Stdlib.Structures.Equalities]
MiniOrderedType.compare [in Stdlib.Structures.OrderedType]
MiniOrderedType.eq [in Stdlib.Structures.OrderedType]
MiniOrderedType.eq_trans [in Stdlib.Structures.OrderedType]
MiniOrderedType.eq_sym [in Stdlib.Structures.OrderedType]
MiniOrderedType.eq_refl [in Stdlib.Structures.OrderedType]
MiniOrderedType.lt [in Stdlib.Structures.OrderedType]
MiniOrderedType.lt_not_eq [in Stdlib.Structures.OrderedType]
MiniOrderedType.lt_trans [in Stdlib.Structures.OrderedType]
MiniOrderedType.t [in Stdlib.Structures.OrderedType]
MSetRemoveMin.remove_min_spec2 [in Stdlib.MSets.MSetRBT]
MSetRemoveMin.remove_min_spec1 [in Stdlib.MSets.MSetRBT]
MSetRemoveMin.remove_min [in Stdlib.MSets.MSetRBT]