∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
[ /3 width=9 by cpx_cpxs, cpx_delta/
∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
[ /3 width=9 by cpx_cpxs, cpx_delta/