proposition: Lemma cons_1 : forall (s:t elt) e, flatten_e (cons s e) = bindings s ++ flatten_e e.
proof: Proof. induction s; auto; intros. simpl flatten_e; rewrite IHs1; apply flatten_e_bindings; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)