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).
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).