∀V,l. ⦃G, K⦄ ⊢ W •*[h, l] V →
∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, l+1] U.
#h #G #L #K #W #i #HLK #V0 #HWV0 #V #l #HWV #U #HVU
∀V,l. ⦃G, K⦄ ⊢ W •*[h, l] V →
∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, l+1] U.
#h #G #L #K #W #i #HLK #V0 #HWV0 #V #l #HWV #U #HVU