nqed.
unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
- R ≟ (mk_unary_morphism1 ?? (composition1 ??? f g)
+ R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g))
(prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
(* -------------------------------------------------------------------- *) ⊢
- fun11 o1 o3 R ≡ (composition1 o1 o2 o3 f g).
+ fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
ndefinition comp1_binary_morphisms:
∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).