proposition: Lemma inter_spec_ok : forall s1 s2 `{Ok s1, Ok s2}, Ok (inter s1 s2) /\ (forall y, InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).
proof: Proof. intros s1 s2; functional induction inter s1 s2; intros B1 B2; [intuition_in|intuition_in | | ]; factornode s2; destruct_split; inv; destruct IHt0 as (IHo1,IHi1), IHt1 as (IHo2,IHi2); auto with *; split; intros. - apply join_ok; auto with *; intro y; rewrite ?IHi1, ?IHi2; intuition. - rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in. setoid_replace y with x1; auto. rewrite <- split_spec3; auto. - apply concat_ok; auto with *; intros y1 y2; rewrite IHi1, IHi2; intuition; order. - rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; auto. intuition_in. absurd (InT x1 s2). + rewrite <- split_spec3; auto; congruence. + setoid_replace x1 with y; auto. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int