apply ((id_neutral_left1 ????)‡#);]
qed.
-definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+ [ apply (ext ? ? (rel o));
+ | intros;
+ apply (.= #‡H);
+ apply refl1]
+qed.
definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
λo.extS ?? (rel o).