proposition: Lemma union_spec: forall x s s', In x (union s s') <-> In x s \/ In x s'.
proof: Proof. unfold In. induction x; destruct s; destruct s'; simpl union; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. apply orb_true_iff. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface