proposition: Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2}, (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).
proof: Proof. intros s1 s2; functional induction union s1 s2; intros y B1 B2. - intuition_in. - intuition_in. - factornode s2; destruct_split; inv. rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *. destruct (X.compare_spec y x1); intuition_in. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int