Back to step 1: all files that used to pass now pass again.

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index c5f125ac679dc3d66c704874d27736a87fa55a67..7e0064e4631429b570248dd4117a88c397521207 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -97,23 +97,23 @@ definition relation_pair_composition:
      | apply (r1 \sub\f ∘ r \sub\f)
      | lapply (commute ?? r) as H;
        lapply (commute ?? r1) as H1;
-       apply rule (.= ASSOC1);
+       apply rule (.= ASSOC);
        apply (.= #‡H1);
-       apply rule (.= ASSOC1\sup -1);
+       apply rule (.= ASSOC ^ -1);
        apply (.= H‡#);
-       apply rule ASSOC1]
+       apply rule ASSOC]
   | intros;
     change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));  
     change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
     change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
-    apply rule (.= ASSOC1);
+    apply rule (.= ASSOC);
     apply (.= #‡e1);
     apply (.= #‡(commute ?? b'));
-    apply rule (.= ASSOC1 \sup -1);
+    apply rule (.= ASSOC \sup -1);
     apply (.= e‡#);
-    apply rule (.= ASSOC1);
+    apply rule (.= ASSOC);
     apply (.= #‡(commute ?? b')\sup -1);
-    apply rule (ASSOC1 \sup -1)]
+    apply rule (ASSOC \sup -1)]
 qed.
     
 definition BP: category2.
@@ -125,7 +125,7 @@ definition BP: category2.
   | intros;
     change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
                  ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
-    apply rule (ASSOC1‡#);
+    apply rule (ASSOC‡#);
   | intros;
     change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
     apply ((id_neutral_right2 ????)‡#);
@@ -184,4 +184,4 @@ qed.
 
 interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
-*)
\ No newline at end of file
+*)