proposition: Lemma equal_spec (m m':t elt)`{!Ok m, !Ok m'} : equal eqb m m' = true <-> Equivb eqb m m'.
proof: Proof. rewrite Equivb_bindings, equal_Leq. split; [apply L.equal_2 | apply L.equal_1]; unfold L.Ok; apply bindings_spec2. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)