X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs.ma;h=3cbb70058ca879290b8f92a8f41d7996fb46e02a;hb=c2123cdb49560cc6ef2a86b71ab21b432581c076;hp=58c4f9c581718941e5df6ff10135aa0e93e44ff2;hpb=62ab884c6ce7dd41c6e6fa2efc5102b23f57de32;p=helm.git

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 58c4f9c58..3cbb70058 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -87,7 +87,7 @@ definition Oid_relation_pair: ∀o:Obasic_pair. Orelation_pair o o.
   | lapply (id_neutral_right2 ? (Oconcr o) ? (⊩)) as H;
     lapply (id_neutral_left2 ?? (Oform o) (⊩)) as H1;
     apply (.= H);
-    apply (H1 \sup -1);]
+    apply (H1^-1);]
 qed.
 
 lemma Orelation_pair_composition:
@@ -121,11 +121,11 @@ intros;
     apply rule (.= ASSOC);
     apply (.= #‡e1);
     apply (.= #‡(Ocommute ?? b'));
-    apply rule (.= ASSOC \sup -1);
+    apply rule (.= ASSOC^-1);
     apply (.= e‡#);
     apply rule (.= ASSOC);
-    apply (.= #‡(Ocommute ?? b')\sup -1);
-    apply rule (ASSOC \sup -1);
+    apply (.= #‡(Ocommute ?? b')^-1);
+    apply rule (ASSOC^-1);
 qed.
 
 definition Orelation_pair_composition_morphism: