-unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
-
-(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
- #A; #A'; #B; #H1; #H2;
- napply (. ((#‡H1)‡H2^-1)); nnormalize;
-nqed.*)
-
-ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
- [ napply Or
- | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
- ##[##1,3: napply or_introl |##*: napply or_intror ]
- ##[ napply (H1 H)
- | napply (H2 H)
- | napply (H3 H)
- | napply (H4 H)]##]
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+ (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
+ (prop11 … and_morphism)
+ A B ≡ And A B.
+
+(*
+naxiom daemon: False.
+
+nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
+nqed.
+
+CSC: ugly proof term
+ncheck test.
+*)
+
+ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … Or);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
+ [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.