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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
index 5f1148dbf..b48aca5c1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
@@ -21,10 +21,10 @@ include "basic_2/substitution/cpy.ma".
 (* Inversion lemmas on negated relocation ***********************************)
 
 lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
-                         ∀i. d ≤ yinj i → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
-                         (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨
-                         ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
-                                    (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
+                         ∀i. d ≤ yinj i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
+                         (∀T1. ⬆[i, 1] T1 ≡ U1 → ⊥) ∨
+                         ∃∃I,K,W,j. d ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W &
+                                    (∀V. ⬆[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥).
 #G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
 [ /3 width=2 by or_introl/
 | #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi #HnW