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 702ca5ab992e29ee0cedf060872dc80aa6abfbdd..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,6 +20,13 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
+| 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