proposition: Lemma remove_min_in : forall l x e r h y, In y (Node l x e r h) <-> X.eq y (remove_min l x e r)#2#1 \/ In y (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. - rewrite e0 in *; simpl; intros. rewrite bal_in, In_node_iff, IHp; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int