update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 98d617600407b05ebe58dea804a1b6c5407ad145..6430cbcd522d339ac5a00da0a9881c8d3f645540 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -20,8 +20,15 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
-lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≡ K →
-                ∀U. ⬆[l, k] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, o].
+| nv_lref: ∀I,G,L,K,V,i. ⬇[i] L ≘ K.ⓑ{I}V → nv a h G K V → nv a h G L (#i)
+
+lemma nv_inv_lref: ∀a,h,G,L,i. ⦃G, L⦄ ⊢ #i ![a, h] →
+                    ∃∃I,K,V. ⬇[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ![a, h].
+/2 width=3 by nv_inv_lref_aux/ qed-.
+
+
+lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≘ K →
+                ∀U. ⬆[l, k] T ≘ U → ⦃G, L⦄ ⊢ U ¡[h, o].
 #h #o #G #K #T #H elim H -G -K -T
 [ #G #K #s #L #b #l #k #_ #X #H
   >(lift_inv_sort1 … H) -X -K -l -k //
@@ -48,8 +55,8 @@ lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l
 ]
 qed.
 
-lemma snv_inv_lift: â\88\80h,o,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, o] â\86\92 â\88\80K,b,l,k. â¬\87[b, l, k] L â\89¡ K →
-                    â\88\80T. â¬\86[l, k] T â\89¡ U → ⦃G, K⦄ ⊢ T ¡[h, o].
+lemma snv_inv_lift: â\88\80h,o,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, o] â\86\92 â\88\80K,b,l,k. â¬\87[b, l, k] L â\89\98 K →
+                    â\88\80T. â¬\86[l, k] T â\89\98 U → ⦃G, K⦄ ⊢ T ¡[h, o].
 #h #o #G #L #U #H elim H -G -L -U
 [ #G #L #s #K #b #l #k #_ #X #H
   >(lift_inv_sort2 … H) -X -L -l -k //