....

[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 58c4f9c581718941e5df6ff10135aa0e93e44ff2..3cbb70058ca879290b8f92a8f41d7996fb46e02a 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
@@ -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: