X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_topologies.ma;h=4c725920bf6346820039542707a98260e25a29dd;hb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;hp=245fc4fdbf866ee9c9a28d521bb790c5f5cf4489;hpb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 245fc4fdb..4c725920b 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -17,11 +17,11 @@ include "o-saturations.ma".
 
 record Obasic_topology: Type2 ≝
  { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒ Ocarrbt;
-   oJ: Ocarrbt ⇒ Ocarrbt;
+   oA: Ocarrbt ⇒_2 Ocarrbt;
+   oJ: Ocarrbt ⇒_2 Ocarrbt;
    oA_is_saturation: is_o_saturation ? oA;
    oJ_is_reduction: is_o_reduction ? oJ;
-   Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+   Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
 record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
@@ -134,11 +134,11 @@ definition OBTop: category2.
        change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
        apply (.= e‡#);
        intro x;          
-       change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x)))); 
+       change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x))); 
        apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply (.= (e1 (a'⎻* (oA o1 x))));
-       change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));   
+       change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));   
        apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply rule #;]