+#S b1 b2; ncases b1; ncases b2;
+nchange in match (true || true) with true;
+nchange in match (true || false) with true;
+nchange in match (ϵ true) with {[]};
+nchange in match (ϵ false) with ∅;
+##[##1,4: napply ((cupID…)^-1);
+##| napply ((cup0 S {[]})^-1);
+##| napply (.= (cup0 S {[]})^-1); napply cupC; ##]
+nqed.
+
+nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c).
+#S a b c; @; #w; *; /3/; *; /3/; nqed.
+
+nlemma setP : ∀S.∀A,B:Ω^S.∀x:S. A = B → (x ∈ A) = (x ∈ B).
+#S A B x; *; #H1 H2; @; ##[ napply H1 | napply H2] nqed.
+
+nlemma pset_ext : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B.
+#S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed.
+
+ndefinition if': ∀A,B:CPROP. A = B → A → B.
+#A B; *; /2/. nqed.
+
+ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?.
+
+(* move in sets.ma? *)
+nlemma union_morphism : ∀A.Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
+#X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
+#A1 A2 B1 B2 EA EB; napply pset_ext; #x;
+nchange in match (x ∈ (A1 ∪ B1)) with (?∨?);
+napply (.= (setP ??? x EA)‡#);
+napply (.= #‡(setP ??? x EB)); //;