-lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
- ∀U. ⬆[l, m] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
-#h #g #G #K #T #H elim H -G -K -T
-[ #G #K #k #L #s #l #m #_ #X #H
- >(lift_inv_sort1 … H) -X -K -l -m //
-| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #l #m #HLK #X #H
+| 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 //
+| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #b #l #k #HLK #X #H