proposition: Lemma cons_1 : forall s e, flatten_e (cons s e) = elements s ++ flatten_e e.
proof: Proof. induction s; simpl; auto; intros. rewrite IHs1; apply flatten_e_elements. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat