X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_cpms.ma;h=e9c66826faee8fa611aa2e4b0a79e9346287b4ef;hp=b87500bd755aeefbec0055f0fabace337058b757;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
index b87500bd7..e9c66826f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
@@ -73,7 +73,7 @@ qed.
 
 (* Basic_2A1: includes: cprs_theta_rc *)
 theorem cpms_theta_rc (n) (h) (G) (L):
-                      ∀V1,V. ❪G,L❫ ⊢ V1 ➡[h] V → ∀V2. ⇧*[1] V ≘ V2 →
+                      ∀V1,V. ❪G,L❫ ⊢ V1 ➡[h] V → ∀V2. ⇧[1] V ≘ V2 →
                       ∀W1,T1,T2. ❪G,L.ⓓW1❫ ⊢ T1 ➡*[n,h] T2 →
                       ∀W2. ❪G,L❫ ⊢ W1 ➡*[h] W2 →
                       ∀p. ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ➡*[n,h] ⓓ[p]W2.ⓐV2.T2.
@@ -86,7 +86,7 @@ qed.
 
 (* Basic_2A1: includes: cprs_theta *)
 theorem cpms_theta (n) (h) (G) (L):
-                   ∀V,V2. ⇧*[1] V ≘ V2 → ∀W1,W2. ❪G,L❫ ⊢ W1 ➡*[h] W2 →
+                   ∀V,V2. ⇧[1] V ≘ V2 → ∀W1,W2. ❪G,L❫ ⊢ W1 ➡*[h] W2 →
                    ∀T1,T2. ❪G,L.ⓓW1❫ ⊢ T1 ➡*[n,h] T2 →
                    ∀V1. ❪G,L❫ ⊢ V1 ➡*[h] V →
                    ∀p. ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ➡*[n,h] ⓓ[p]W2.ⓐV2.T2.
@@ -121,7 +121,7 @@ lemma cpms_inv_appl_sn (n) (h) (G) (L):
                             ❪G,L❫ ⊢ T1 ➡*[n1,h] ⓛ[p]W.T & ❪G,L❫ ⊢ ⓓ[p]ⓝW.V1.T ➡*[n2,h] X2 &
                             n1 + n2 = n
                         | ∃∃n1,n2,p,V0,V2,V,T.
-                            ❪G,L❫ ⊢ V1 ➡*[h] V0 & ⇧*[1] V0 ≘ V2 &
+                            ❪G,L❫ ⊢ V1 ➡*[h] V0 & ⇧[1] V0 ≘ V2 &
                             ❪G,L❫ ⊢ T1 ➡*[n1,h] ⓓ[p]V.T & ❪G,L❫ ⊢ ⓓ[p]V.ⓐV2.T ➡*[n2,h] X2 &
                             n1 + n2 = n.
 #n #h #G #L #V1 #T1 #U2 #H