proposition: Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2).
proof: Proof. intros m1 m2; functional induction (merge m1 m2); intros; try factornode _x _x0 _x1 _x2 _x3 as m1. - intuition_in. - intuition_in. - rewrite bal_mapsto, remove_min_mapsto, e1; simpl; auto. unfold create. intuition; subst; auto. inversion_clear H1; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int