∀P,Q. arrows1 BP P Q → relation_pair_setoid P Q ≝ λP,Q,x.x.
coercion relation_pair_setoid_of_arrows1_BP.
+(*
definition BPext: ∀o: BP. (form o) ⇒_1 Ω^(concr o).
intros; constructor 1;
[ apply (ext ? ? (rel o));
interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr ?) ?? (relS c) x y).
interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ??? (relS c)).
+*)