X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Foverlap%2Fo-algebra.ma;h=40b2f72bb5dab9c2d53b979059e9b88bf0b7c063;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=54e920c2e315c41db5c176a62dae55265a04f317;hpb=d3186f4cfe51f34b7aa828242c2fcc9b415568f2;p=helm.git

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index 54e920c2e..40b2f72bb 100644
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -220,7 +220,7 @@ nlemma ORelation_eq2:
   r=r' → r⎻ = r'⎻.
  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -259,7 +259,7 @@ nlemma ORelation_eq3:
   r=r' → r* = r'*.
  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -295,7 +295,7 @@ nlemma ORelation_eq4:
   r=r' → r⎻* = r'⎻*.
  #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_star_morphism1: