X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs.ma;h=8e5421c1f0b39617a9896c045a7070b64c606061;hb=82b1a205fdf9bc2c8029296ebe94c5667798845b;hp=44f8e9f213aa2753789d4b1b83b727cdc32a4da3;hpb=5027bc68bf4f3dc777d35476a2fb8a41b6bc1e29;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 44f8e9f21..8e5421c1f 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -172,6 +172,7 @@ definition relation_pair_setoid_of_arrows1_BP :
   ∀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));
@@ -219,3 +220,4 @@ qed.
 
 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)).
+*)