- | ∃∃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] ⓛ{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.