notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / cpy_nlift.ma

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 5f1148dbf260d46656bce852484cad6cee7931ad..b48aca5c192f310972c2907d9beee864bb0e6dfd 100644 (file)
--- 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 →
-                         â\88\80i. d â\89¤ yinj i â\86\92 (â\88\80T2. â\87§[i, 1] T2 ≡ U2 → ⊥) →
-                         (â\88\80T1. â\87§[i, 1] T1 ≡ U1 → ⊥) ∨
-                         â\88\83â\88\83I,K,W,j. d â\89¤ yinj j & j < i & â\87©[j]L ≡ K.ⓑ{I}W &
-                                    (â\88\80V. â\87§[i-j-1, 1] V â\89¡ W â\86\92 â\8a¥) & (â\88\80T1. â\87§[j, 1] T1 ≡ U1 → ⊥).
+                         â\88\80i. d â\89¤ yinj i â\86\92 (â\88\80T2. â¬\86[i, 1] T2 ≡ U2 → ⊥) →
+                         (â\88\80T1. â¬\86[i, 1] T1 ≡ U1 → ⊥) ∨
+                         â\88\83â\88\83I,K,W,j. d â\89¤ yinj j & j < i & â¬\87[j]L ≡ K.ⓑ{I}W &
+                                    (â\88\80V. â¬\86[i-j-1, 1] V â\89¡ W â\86\92 â\8a¥) & (â\88\80T1. â¬\86[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