proposition: Lemma Simplify_add : forall (X X0:Ensemble U) (x:U), ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
proof: Proof. intros X X0 x H' H'0 H'1; try assumption. rewrite (Sub_Add_new X x); auto with sets. rewrite (Sub_Add_new X0 x); auto with sets. rewrite H'1; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets