notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
index 1b66bd0b74d911d9a158ae103f04ee127deb7d19..14b5eff6c67e949138651772bedd116dbb26de49 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
@@ -52,7 +52,7 @@ lemma frees_dec: ∀L,U,d,i. Decidable (frees d L U i).
 ]
 qed-.
 
-lemma frees_S: â\88\80L,U,d,i. L â\8a¢ i ϵ ð\9d\90\85*[yinj d]â¦\83Uâ¦\84 â\86\92 â\88\80I,K,W. â\87©[d] L ≡ K.ⓑ{I}W →
+lemma frees_S: â\88\80L,U,d,i. L â\8a¢ i ϵ ð\9d\90\85*[yinj d]â¦\83Uâ¦\84 â\86\92 â\88\80I,K,W. â¬\87[d] L ≡ K.ⓑ{I}W →
                (K ⊢ i-d-1 ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯d]⦃U⦄.
 #L #U #d #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
 * #I #K #W #j #Hdj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
@@ -75,8 +75,8 @@ qed.
 (* Properties on relocation *************************************************)
 
 lemma frees_lift_ge: ∀K,T,d,i. K ⊢ i ϵ𝐅*[d]⦃T⦄ →
-                     â\88\80L,s,d0,e0. â\87©[s, d0, e0] L ≡ K →
-                     â\88\80U. â\87§[d0, e0] T ≡ U → d0 ≤ i →
+                     â\88\80L,s,d0,e0. â¬\87[s, d0, e0] L ≡ K →
+                     â\88\80U. â¬\86[d0, e0] T ≡ U → d0 ≤ i →
                      L ⊢ i+e0 ϵ 𝐅*[d]⦃U⦄.
 #K #T #d #i #H elim H -K -T -d -i
 [ #K #T #d #i #HnT #L #s #d0 #e0 #_ #U #HTU #Hd0i -K -s
@@ -103,8 +103,8 @@ qed.
 (* Inversion lemmas on relocation *******************************************)
 
 lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
-                         â\88\80K,s,d0,e0. â\87©[s, d0, e0+1] L ≡ K →
-                         â\88\80T. â\87§[d0, e0+1] T ≡ U → d0 ≤ i → i ≤ d0 + e0 → ⊥.
+                         â\88\80K,s,d0,e0. â¬\87[s, d0, e0+1] L ≡ K →
+                         â\88\80T. â¬\86[d0, e0+1] T ≡ U → d0 ≤ i → i ≤ d0 + e0 → ⊥.
 #L #U #d #i #H elim H -L -U -d -i
 [ #L #U #d #i #HnU #K #s #d0 #e0 #_ #T #HTU #Hd0i #Hide0
   elim (lift_split … HTU i e0) -HTU /2 width=2 by/
@@ -121,8 +121,8 @@ lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
 qed-.
 
 lemma frees_inv_lift_ge: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
-                         â\88\80K,s,d0,e0. â\87©[s, d0, e0] L ≡ K →
-                         â\88\80T. â\87§[d0, e0] T ≡ U → d0 + e0 ≤ i →
+                         â\88\80K,s,d0,e0. â¬\87[s, d0, e0] L ≡ K →
+                         â\88\80T. â¬\86[d0, e0] T ≡ U → d0 + e0 ≤ i →
                          K ⊢ i-e0 ϵ𝐅*[d-yinj e0]⦃T⦄.
 #L #U #d #i #H elim H -L -U -d -i
 [ #L #U #d #i #HnU #K #s #d0 #e0 #HLK #T #HTU #Hde0i -L -s