-ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
- [ napply (λA,B. A → B)
- | #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
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+ (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+ (prop11 … if_morphism)
+ A B ≡ A → B.
\ No newline at end of file