proposition: Lemma remove_min_spec : forall l x r y h, InT y (Node h l x r) <-> X.eq y (remove_min l x r)#2 \/ InT y (remove_min l x r)#1.
proof: Proof. intros l x r; functional induction (remove_min l x r); simpl in *; intros. - intuition_in. - rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int