- ∀W1,T1,X2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[n,h] X2 →
- ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[n,h] W2 & ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓝW2.T2
- | ⦃G, L⦄ ⊢ T1 ➡*[n,h] X2
- | ∃∃m. ⦃G, L⦄ ⊢ W1 ➡*[m,h] X2 & n = ↑m.
+ ∀W1,T1,X2. ⦃G,L⦄ ⊢ ⓝW1.T1 ➡*[n,h] X2 →
+ ∨∨ ∃∃W2,T2. ⦃G,L⦄ ⊢ W1 ➡*[n,h] W2 & ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓝW2.T2
+ | ⦃G,L⦄ ⊢ T1 ➡*[n,h] X2
+ | ∃∃m. ⦃G,L⦄ ⊢ W1 ➡*[m,h] X2 & n = ↑m.