ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))).
*)
ndefinition ORelation_composition : ∀P,Q,R.
ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))).
*)
ndefinition ORelation_composition : ∀P,Q,R.