proposition: Lemma equal_spec : forall (A:Type)(cmp:A->A->bool)(m m':t A), equal cmp m m' = true <-> Equivb cmp m m'.
proof: Proof. split. apply equal_2. apply equal_1. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)