X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_cpms.ma;h=8273d996b7b505f42689a917380395f7a29331ce;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=0e09b27f0835401c3ace850d4ded61fecde069e3;hpb=db020b4218272e2e35641ce3bc3b0a9b3afda899;p=helm.git

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 0e09b27f0..8273d996b 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
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_3_5.ma".
 include "ground_2/xoa/ex_5_7.ma".
 include "basic_2/rt_transition/cpm_lsubr.ma".
 include "basic_2/rt_computation/cpms_drops.ma".
@@ -72,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.
@@ -85,9 +86,9 @@ 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 → 
+                   ∀V1. ⦃G,L⦄ ⊢ V1 ➡*[h] V →
                    ∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.
 #n #h #G #L #V #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #HT12 #V1 #H @(cprs_ind_sn … H) -V1
 [ /2 width=3 by cpms_theta_rc/
@@ -120,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