X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lift.ma;h=6430cbcd522d339ac5a00da0a9881c8d3f645540;hb=e62715437a9c39244c9809c00585a5ef44a39797;hp=98d617600407b05ebe58dea804a1b6c5407ad145;hpb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;p=helm.git

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 98d617600..6430cbcd5 100644
--- 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: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≡ K →
-                    ∀T. ⬆[l, k] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, o].
+lemma snv_inv_lift: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≘ K →
+                    ∀T. ⬆[l, k] T ≘ 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 //