+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ o1,o2 ;
+ X ≟ unary_morph_setoid o1 o2
+ (* ----------------------------- *) ⊢
+ carr X ≡ o1 ⇒_0 o2.
+
+interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
+interpretation "prop2_x0" 'prop2_x0 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
+
+nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g.
+#A B f g H x1 x2 E; napply (.= †E); napply H; nqed.
+
+nlemma mk_binary_morphism:
+ ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
+ A ⇒_0 (unary_morph_setoid B C).
+ #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ /2/.
+nqed.