proposition: Lemma remove_min_mapsto : forall l x e r h y e', MapsTo y e' (Node l x e r h) <-> ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2) \/ MapsTo y e' (remove_min l x e r)#1.
proof: Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. - intuition_in; subst; auto. - rewrite e0 in *; simpl; intros. rewrite bal_mapsto; auto; unfold create. simpl in *;destruct (IHp _x y e'). intuition. + inversion_clear H1; intuition. + inversion_clear H3; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int