proposition: Theorem Triple_as_Couple_Singleton : forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
proof: Proof. intros x y z. rewrite <- (Triple_as_union x y z). rewrite <- (Couple_as_union x y); auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset