X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fcpys.ma;h=eda8ee1e14a87513af7465b2aab1fad673e13c2b;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=c7d59d176b905b282e1ba69a00ed1c53585af5b7;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
index c7d59d176..eda8ee1e1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
@@ -98,9 +98,9 @@ qed-.
 (* Basic forward lemmas *****************************************************)
 
 lemma cpys_fwd_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                   ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                   ∀T1,d,e. ⬆[d, e] T1 ≡ U1 →
                    d ≤ dt → d + e ≤ dt + et →
-                   ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2.
+                   ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*[d+e, dt+et-(d+e)] U2 & ⬆[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU
@@ -160,7 +160,7 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*[d, 0] T2 → T1 =
 qed-.
 
 lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat.
-                         ⦃G, L⦄ ⊢ U1 ▶*[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
+                         ⦃G, L⦄ ⊢ U1 ▶*[d, e] U2 → ∀T1. ⬆[d, e] T1 ≡ U1 → U1 = U2.
 #G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2
 /2 width=7 by cpy_inv_lift1_eq/
 qed-.