- binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2)
- (unary_morphism1_setoid1 o1 o3).
-#o1; #o2; #o3; @
+ unary_morphism1 (unary_morphism1_setoid1 o2 o3)
+ (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+#o1; #o2; #o3; napply mk_binary_morphism1