nqed.
unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
- R ≟ mk_unary_morphism ?? (composition ??? f g)
- (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+ R ≟ mk_unary_morphism o1 o3
+ (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+ (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
(* -------------------------------------------------------------------- *) ⊢
- fun1 o1 o3 R ≡ (composition o1 o2 o3 f g).
+ fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
ndefinition comp_binary_morphisms:
∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).