...

[helm.git] / helm / software / matita / nlibrary / overlap / o-algebra.ma

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index 54e920c2e315c41db5c176a62dae55265a04f317..40b2f72bb5dab9c2d53b979059e9b88bf0b7c063 100644 (file)
--- 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: