apply e;
qed.
-theorem BP_to_OBP_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
+theorem BP_to_OBP_full:
+ ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
intros;
cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);