proposition: Lemma diff_spec : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (diff s s') <-> In x s /\ ~In x s'.
proof: Proof. unfold diff; intros s s'; revert s. induction s'; simpl; unfold flip. - intuition; inv. - intros. inv. rewrite IHs', remove_spec, InA_cons; intuition. Qed.
imports: MSetInterface