proposition: Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
proof: Proof. intro x; rewrite (Empty_set_zero' x); auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset