proposition: Lemma inter_spec: forall s s' x, In x (inter 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'; simpl inter; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. apply andb_true_iff. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface