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