- | ∃∃cV,i,K,V,V2. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬈[Rt,cV,h] V2 &
- ⇧*[↑i] V2 ≘ T2 & I = LRef i & c = cV
- | ∃∃cV,i,K,V,V2. ⇩*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬈[Rt,cV,h] V2 &
- ⇧*[↑i] V2 ≘ T2 & I = LRef i & c = cV + 𝟘𝟙.
+ | ∃∃cV,i,K,V,V2. ⇩[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ⬈[Rt,cV,h] V2 &
+ ⇧[↑i] V2 ≘ T2 & I = LRef i & c = cV
+ | ∃∃cV,i,K,V,V2. ⇩[i] L ≘ K.ⓛV & ❪G,K❫ ⊢ V ⬈[Rt,cV,h] V2 &
+ ⇧[↑i] V2 ≘ T2 & I = LRef i & c = cV + 𝟘𝟙.