proposition: Lemma merge_spec : forall s1 s2 y, InT y (merge s1 s2) <-> InT y s1 \/ InT y s2.
proof: Proof. intros s1 s2; functional induction (merge s1 s2); intros; try factornode s1. - intuition_in. - intuition_in. - rewrite bal_spec, remove_min_spec, e1; simpl; intuition. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int