notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
index d58e5ac2ac8199a9b5edbf30324194f2f44e5fcf..88d4db42136f98153d6ef97e8bb992680198746d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
@@ -20,12 +20,12 @@ include "basic_2/computation/scpds.ma".
 (* activate genv *)
 inductive snv (h) (g): relation3 genv lenv term ≝
 | snv_sort: ∀G,L,k. snv h g G L (⋆k)
-| snv_lref: â\88\80I,G,L,K,V,i. â\87©[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
+| snv_lref: â\88\80I,G,L,K,V,i. â¬\87[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
 | snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T)
 | snv_appl: ∀a,G,L,V,W0,T,U0,l. snv h g G L V → snv h g G L T →
             ⦃G, L⦄ ⊢ V •*➡*[h, g, 1] W0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W0.U0 → snv h g G L (ⓐV.T)
 | snv_cast: ∀G,L,U,T,U0. snv h g G L U → snv h g G L T →
-            â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡* U0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0 → snv h g G L (ⓝU.T)
+            â¦\83G, Lâ¦\84 â\8a¢ U â\80¢*â\9e¡*[h, g, 0] U0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0 → snv h g G L (ⓝU.T)
 .
 
 interpretation "stratified native validity (term)"
@@ -34,7 +34,7 @@ interpretation "stratified native validity (term)"
 (* Basic inversion lemmas ***************************************************)
 
 fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i →
-                       â\88\83â\88\83I,K,V. â\87©[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+                       â\88\83â\88\83I,K,V. â¬\87[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
 #h #g #G #L #X * -G -L -X
 [ #G #L #k #i #H destruct
 | #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/
@@ -45,7 +45,7 @@ fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i
 qed-.
 
 lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] →
-                    â\88\83â\88\83I,K,V. â\87©[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+                    â\88\83â\88\83I,K,V. â¬\87[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
 /2 width=3 by snv_inv_lref_aux/ qed-.
 
 fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥.
@@ -95,7 +95,7 @@ lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] →
 
 fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀U,T. X = ⓝU.T →
                        ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
-                             â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡* U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
+                             â¦\83G, Lâ¦\84 â\8a¢ U â\80¢*â\9e¡*[h, g, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
 #h #g #G #L #X * -G -L -X
 [ #G #L #k #X1 #X2 #H destruct
 | #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
@@ -107,5 +107,5 @@ qed-.
 
 lemma snv_inv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] →
                     ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
-                          â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡* U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
+                          â¦\83G, Lâ¦\84 â\8a¢ U â\80¢*â\9e¡*[h, g, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
 /2 width=3 by snv_inv_cast_aux/ qed-.