X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fbasic_pairs.ma;h=0d51724de7114ad3eb7c2d3936856a13933ed313;hb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;hp=475445720202266f7b9503b696d2e66c21fb2ab9;hpb=1110bdf814f976ef0a36a024d2cba847ce06347e;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 475445720..0d51724de 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -133,7 +133,13 @@ definition BP: category1.
     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).