| napply (H4 K2)]##]
nqed.
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+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.*)
-(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
-
ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
napply mk_binary_morphism1
[ napply Or
| napply (H4 H)]##]
nqed.
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
-
-(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B.
ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
napply mk_binary_morphism1
| #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
[ napply (if … H2); napply H; napply (fi … H1); nassumption
| napply (fi … H2); napply H; napply (if … H1); nassumption]##]
-nqed.
\ No newline at end of file
+nqed.