X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Facp_cr.ma;h=5b8a2c1ea3652235976d2e5c5665d03a704ed3cb;hb=cb38da6095e3af84131a3ebf47a9f252f34a804c;hp=1805953b99870cee59fa5328d9a3990cbd8afff1;hpb=db7ecce6c398a42f14557067bf18b61cf75da80e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
index 1805953b9..5b8a2c1ea 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
@@ -42,7 +42,7 @@ definition S5 ≝ λRP,C:lenv→predicate term.
                 ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
 
 definition S6 ≝ λRP,C:lenv→predicate term.
-                ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓣW. T).
+                ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T).
 
 definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
                 C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.