- | ∃∃p,W,T. ❪G,L❫ ⊢ T1 ➡*[h] ⓛ[p]W.T &
- ❪G,L❫ ⊢ ⓓ[p]ⓝW.V1.T ➡*[h] X2
- | ∃∃p,V0,V2,V,T. ❪G,L❫ ⊢ V1 ➡*[h] V0 & ⇧[1] V0 ≘ V2 &
- ❪G,L❫ ⊢ T1 ➡*[h] ⓓ[p]V.T &
- ❪G,L❫ ⊢ ⓓ[p]V.ⓐV2.T ➡*[h] X2.
+ | ∃∃p,W,T. ❪G,L❫ ⊢ T1 ➡*[h,0] ⓛ[p]W.T &
+ ❪G,L❫ ⊢ ⓓ[p]ⓝW.V1.T ➡*[h,0] X2
+ | ∃∃p,V0,V2,V,T. ❪G,L❫ ⊢ V1 ➡*[h,0] V0 & ⇧[1] V0 ≘ V2 &
+ ❪G,L❫ ⊢ T1 ➡*[h,0] ⓓ[p]V.T &
+ ❪G,L❫ ⊢ ⓓ[p]V.ⓐV2.T ➡*[h,0] X2.