...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / r-o-basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index bba4662697af1fe19b89ce0f963878237da05453..1dcc1b91fe3c8a1c45746453190a1c16151c5faa 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -20,12 +20,12 @@ definition rOBP ≝ Apply ?? BP_to_OBP.
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
 lemma rOR_full : 
-  ∀rS,rT:rOBP.∀f:arrows2 ? (OR (F2 ??? rS)) (OR (F2 ??? rT)).
-    exT22 ? (λg:arrows2 OBP (F1 ??? rS) (F1 ??? rT).
-       map_arrows2 ? ? OR rS rT g = f).
-  ∀S,T.∀f. exT22 ? (λg. map_arrows2 ? ? OR S T g = f).
-arrows2 OBP S T
-unary_morphism1_setoid1 (OR S) (OR T)
+  ∀rS,rT:rOBP.∀f:arrows2 BTop (OR (ℱ_2 rS)) (OR (ℱ_2 rT)).
+    exT22 ? (λg:arrows2 rOBP rS rT.
+       map_arrows2 ?? OR ?? (ℳ_2 g) = f).
+intros; cases f (c H1 H2); simplify;
+STOP;
+ 
 
 (* Todo: rename BTop → OBTop *)