proposition: Lemma flatten_e_elements : forall (l:t elt) r x d z e, elements l ++ flatten_e (More x d r e) = elements (Node l x d r z) ++ flatten_e e.
proof: Proof. intros; apply elements_node. Qed.
imports: FunInd FMapInterface FMapList ZArith Int