proposition: Lemma Add_inv : forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
proof: Proof. intros A x y H'; induction H'. - left; assumption. - right; apply Singleton_inv; assumption. Qed.
imports: Ensembles