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