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. induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto; try sort_inf_in; try order. right; intuition; inv; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists