proposition: Lemma diff_spec: forall s s' x, In x (diff s s') <-> In x s /\ ~ In x s'.
proof: Proof. unfold In. intros s s' x; revert x s s'. induction x; destruct s; destruct s' as [|l' o' r']; simpl diff; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. rewrite andb_true_iff. destruct o'; intuition discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface