proposition: Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
proof: Proof. unfold Add at 1; auto using Empty_set_zero with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset