- ∀X. ❪G,L❫ ⊢ ⓝU1.T1 ➡[n,h] X → ⓝU1.T1 ≛ X →
- ∃∃U0,U2,T2. ❪G,L❫ ⊢ U1 ➡*[h] U0 & ❪G,L❫ ⊢ T1 ➡*[1,h] U0
- & ❪G,L❫ ⊢ U1 ![h,a] & ❪G,L❫ ⊢ U1 ➡[n,h] U2 & U1 ≛ U2
- & ❪G,L❫ ⊢ T1 ![h,a] & ❪G,L❫ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓝU2.T2.
+ ∀X. ❪G,L❫ ⊢ ⓝU1.T1 ➡[h,n] X → ⓝU1.T1 ≛ X →
+ ∃∃U0,U2,T2. ❪G,L❫ ⊢ U1 ➡*[h,0] U0 & ❪G,L❫ ⊢ T1 ➡*[h,1] U0
+ & ❪G,L❫ ⊢ U1 ![h,a] & ❪G,L❫ ⊢ U1 ➡[h,n] U2 & U1 ≛ U2
+ & ❪G,L❫ ⊢ T1 ![h,a] & ❪G,L❫ ⊢ T1 ➡[h,n] T2 & T1 ≛ T2 & X = ⓝU2.T2.