proposition: Lemma equal_Leq m1 m2 : equal eqb m1 m2 = Leq (bindings m1) (bindings m2).
proof: Proof. unfold equal. rewrite <- (app_nil_r (bindings m1)). replace (bindings m2) with (flatten_e (cons m2 (End _))) by (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply equal_cont_Leq. now destruct e. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)