X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms.ma;h=081eece9b1257698327268c01aa216e38beeafc5;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=d422aaf2221049b8fa841af761031b403f003408;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
index d422aaf22..081eece9b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
@@ -80,7 +80,7 @@ lemma cpms_appl_dx (n) (h) (G) (L):
 qed.
 
 lemma cpms_zeta (n) (h) (G) (L):
-                ∀T1,T. ⬆*[1] T ≘ T1 →
+                ∀T1,T. ⇧*[1] T ≘ T1 →
                 ∀V,T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[n,h] T2.
 #n #h #G #L #T1 #T #HT1 #V #T2 #H @(cpms_ind_dx … H) -T2
 /3 width=3 by cpms_step_dx, cpm_cpms, cpm_zeta/
@@ -88,7 +88,7 @@ qed.
 
 (* Basic_2A1: uses: cprs_zeta *)
 lemma cpms_zeta_dx (n) (h) (G) (L):
-                   ∀T2,T. ⬆*[1] T2 ≘ T →
+                   ∀T2,T. ⇧*[1] T2 ≘ T →
                    ∀V,T1. ⦃G,L.ⓓV⦄ ⊢ T1 ➡*[n,h] T → ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[n,h] T2.
 #n #h #G #L #T2 #T #HT2 #V #T1 #H @(cpms_ind_sn … H) -T1
 /3 width=3 by cpms_step_sn, cpm_cpms, cpm_bind, cpm_zeta/
@@ -125,7 +125,7 @@ qed.
 (* Basic_2A1: uses: cprs_theta_dx *)
 lemma cpms_theta_dx (n) (h) (G) (L):
                     ∀V1,V. ⦃G,L⦄ ⊢ V1 ➡[h] V →
-                    ∀V2. ⬆*[1] V ≘ V2 →
+                    ∀V2. ⇧*[1] V ≘ V2 →
                     ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡[h] W2 →
                     ∀T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 →
                     ∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.