proposition: Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
proof: Proof. intros x y. rewrite <- (Couple_as_union x y). rewrite <- (Union_idempotent (Singleton U x)). apply Triple_as_union. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset