proposition: Lemma inter_spec : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (inter s s') <-> In x s /\ In x s'.
proof: Proof. unfold inter, fold, flip; intros. set (acc := nil (A:=elt)) in *. assert (Hacc : Ok acc) by constructors. assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc). { intuition; unfold acc in *; inv. } rewrite IFF; clear IFF. clearbody acc. revert acc Hacc x s' Hs Hs'. induction s; simpl; intros. - intuition; inv. - inv. case_eq (mem a s'); intros Hm. + rewrite IHs, add_spec, InA_cons; intuition. rewrite mem_spec in Hm; auto. left; split; auto. rewrite H1; auto. + rewrite IHs, InA_cons; intuition. rewrite H2, <- mem_spec in H3; auto. congruence. Qed.
imports: MSetInterface