notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / frees.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma
index b803a05b6e53cedfefc69fcec27185f5b5d97151..f7269bc09050092caa706acdf83e06b3d6789da7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma
@@ -20,9 +20,9 @@ include "basic_2/substitution/drop.ma".
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
 inductive frees: relation4 ynat lenv term nat ≝
-| frees_eq: â\88\80L,U,d,i. (â\88\80T. â\87§[i, 1] T ≡ U → ⊥) → frees d L U i
+| frees_eq: â\88\80L,U,d,i. (â\88\80T. â¬\86[i, 1] T ≡ U → ⊥) → frees d L U i
 | frees_be: ∀I,L,K,U,W,d,i,j. d ≤ yinj j → j < i →
-            (â\88\80T. â\87§[j, 1] T â\89¡ U â\86\92 â\8a¥) â\86\92 â\87©[j]L ≡ K.ⓑ{I}W →
+            (â\88\80T. â¬\86[j, 1] T â\89¡ U â\86\92 â\8a¥) â\86\92 â¬\87[j]L ≡ K.ⓑ{I}W →
             frees 0 K W (i-j-1) → frees d L U i.
 
 interpretation
@@ -35,9 +35,9 @@ definition frees_trans: predicate (relation3 lenv term term) ≝
 (* Basic inversion lemmas ***************************************************)
 
 lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
-                 (â\88\80T. â\87§[i, 1] T ≡ U → ⊥) ∨
-                 â\88\83â\88\83I,K,W,j. d â\89¤ yinj j & j < i & (â\88\80T. â\87§[j, 1] T ≡ U → ⊥) &
-                            â\87©[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+                 (â\88\80T. â¬\86[i, 1] T ≡ U → ⊥) ∨
+                 â\88\83â\88\83I,K,W,j. d â\89¤ yinj j & j < i & (â\88\80T. â¬\86[j, 1] T ≡ U → ⊥) &
+                            â¬\87[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
 #L #U #d #i * -L -U -d -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
 qed-.
 
@@ -51,7 +51,7 @@ qed-.
 
 lemma frees_inv_lref: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ →
                       j = i ∨
-                      â\88\83â\88\83I,K,W. d â\89¤ yinj j & j < i & â\87©[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+                      â\88\83â\88\83I,K,W. d â\89¤ yinj j & j < i & â¬\87[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
 #L #d #x #i #H elim (frees_inv … H) -H
 [ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
 | * #I #K #W #j #Hdj #Hji #Hnx #HLK #HW
@@ -76,7 +76,7 @@ lemma frees_inv_lref_ge: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → i ≤ j →
 qed-.
 
 lemma frees_inv_lref_lt: ∀L,d,j,i.L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → j < i →
-                         â\88\83â\88\83I,K,W. d â\89¤ yinj j & â\87©[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+                         â\88\83â\88\83I,K,W. d â\89¤ yinj j & â¬\87[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
 #L #d #j #i #H #Hji elim (frees_inv_lref … H) -H
 [ #H elim (lt_refl_false j) //
 | * /2 width=5 by ex3_3_intro/
@@ -114,7 +114,7 @@ qed-.
 lemma frees_lref_eq: ∀L,d,i. L ⊢ i ϵ 𝐅*[d]⦃#i⦄.
 /3 width=7 by frees_eq, lift_inv_lref2_be/ qed.
 
-lemma frees_lref_be: â\88\80I,L,K,W,d,i,j. d â\89¤ yinj j â\86\92 j < i â\86\92 â\87©[j]L ≡ K.ⓑ{I}W →
+lemma frees_lref_be: â\88\80I,L,K,W,d,i,j. d â\89¤ yinj j â\86\92 j < i â\86\92 â¬\87[j]L ≡ K.ⓑ{I}W →
                      K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[d]⦃#j⦄.
 /3 width=9 by frees_be, lift_inv_lref2_be/ qed.