proposition: Lemma equal_cont_Leq : forall m1 cont e2 l, (forall e, cont e = Leq l (flatten_e e)) -> equal_cont eqb m1 cont e2 = Leq (bindings m1 ++ l) (flatten_e e2).
proof: Proof. induction m1 as [|h1 l1 Hl1 x1 d1 r1 Hr1]; intros; auto. rewrite bindings_node_acc; simpl. apply Hl1; auto. clear e2; intros [|x2 d2 r2 e2]; simpl; auto. case K.compare; auto. rewrite <- andb_lazy_alt. f_equal. rewrite <- cons_1; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)