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