+interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
+
+nlemma unary_morph1_eq1: ∀A,B.∀f,g: unary_morphism1 A B. (∀x. f x = g x) → f=g.
+/3/. nqed.
+
+nlemma mk_binary_morphism1:
+ ∀A,B,C: setoid1. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
+ unary_morphism1 A (unary_morphism1_setoid1 B C).
+ #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph1_eq1; #y]
+ /2/.
+nqed.
+