-lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
- ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ T ¡[g].
-#h #g #L #U #H elim H -L -U
-[ #L #k #K #d #e #_ #X #H
+lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
+#h #g #G #L #U #H elim H -G -L -U
+[ #G #L #k #K #s #d #e #_ #X #H