proposition: Lemma equal_2 m m' cmp : equal cmp m m' = true -> Equivb cmp m m'.
proof: Proof. apply equal_spec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)