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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
index bbf9483b2..e872f21c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
@@ -90,7 +90,7 @@ lemma cpxs_pair_sn: ∀h,I,G,L,V1,V2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 →
 qed.
 
 lemma cpxs_zeta (h) (G) (L) (V):
-                ∀T1,T. ⇧*[1] T ≘ T1 →
+                ∀T1,T. ⇧[1] T ≘ T1 →
                 ∀T2. ❪G,L❫ ⊢ T ⬈*[h] T2 → ❪G,L❫ ⊢ +ⓓV.T1 ⬈*[h] T2.
 #h #G #L #V #T1 #T #HT1 #T2 #H @(cpxs_ind … H) -T2
 /3 width=3 by cpxs_strap1, cpx_cpxs, cpx_zeta/
@@ -98,7 +98,7 @@ qed.
 
 (* Basic_2A1: was: cpxs_zeta *)
 lemma cpxs_zeta_dx (h) (G) (L) (V):
-                   ∀T2,T. ⇧*[1] T2 ≘ T →
+                   ∀T2,T. ⇧[1] T2 ≘ T →
                    ∀T1. ❪G,L.ⓓV❫ ⊢ T1 ⬈*[h] T → ❪G,L❫ ⊢ +ⓓV.T1 ⬈*[h] T2.
 #h #G #L #V #T2 #T #HT2 #T1 #H @(cpxs_ind_dx … H) -T1
 /3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
@@ -125,7 +125,7 @@ lemma cpxs_beta_dx: ∀h,p,G,L,V1,V2,W1,W2,T1,T2.
 qed.
 
 lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
-                     ❪G,L❫ ⊢ V1 ⬈[h] V → ⇧*[1] V ≘ V2 → ❪G,L.ⓓW1❫ ⊢ T1 ⬈*[h] T2 →
+                     ❪G,L❫ ⊢ V1 ⬈[h] V → ⇧[1] V ≘ V2 → ❪G,L.ⓓW1❫ ⊢ T1 ⬈*[h] T2 →
                      ❪G,L❫ ⊢ W1 ⬈[h] W2 → ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ⬈*[h] ⓓ[p]W2.ⓐV2.T2.
 #h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
 /4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/