proposition: Lemma append_mapsto m1 m2 y e : MapsTo y e (append m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2.
proof: Proof. functional induction (append m1 m2); intros; try factornode m1. - intuition_m. - intuition_m. - factor_remove_min l R. rewrite bal_mapsto, (remove_min_mapsto R). simpl. unfold create; intuition_m. subst. now constructor. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)