+(*
+definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
+coercion setoid_of_REL.
+*)
+
+definition binary_relation_setoid_of_arrow1_REL :
+ ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.
+coercion binary_relation_setoid_of_arrow1_REL.
+