∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs