- ∀V1. ❪G0,L0❫ ⊢ V0 ➡[h] V1 → ∀U1. ⇧[1] V1 ≘ U1 →
- ∀W1. ❪G0,L0❫ ⊢ W0 ➡[h] W1 → ∀T1. ❪G0,L0.ⓓW0❫ ⊢ T0 ➡[h] T1 →
- ∀V2. ❪G0,L0❫ ⊢ V0 ➡[h] V2 → ∀U2. ⇧[1] V2 ≘ U2 →
- ∀W2. ❪G0,L0❫ ⊢ W0 ➡[h] W2 → ∀T2. ❪G0,L0.ⓓW0❫ ⊢ T0 ➡[h] T2 →
- ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 →
- ∃∃T. ❪G0,L1❫ ⊢ ⓓ[p]W1.ⓐU1.T1 ➡[h] T & ❪G0,L2❫ ⊢ ⓓ[p]W2.ⓐU2.T2 ➡[h] T.
+ ∀V1. ❪G0,L0❫ ⊢ V0 ➡[h,0] V1 → ∀U1. ⇧[1] V1 ≘ U1 →
+ ∀W1. ❪G0,L0❫ ⊢ W0 ➡[h,0] W1 → ∀T1. ❪G0,L0.ⓓW0❫ ⊢ T0 ➡[h,0] T1 →
+ ∀V2. ❪G0,L0❫ ⊢ V0 ➡[h,0] V2 → ∀U2. ⇧[1] V2 ≘ U2 →
+ ∀W2. ❪G0,L0❫ ⊢ W0 ➡[h,0] W2 → ∀T2. ❪G0,L0.ⓓW0❫ ⊢ T0 ➡[h,0] T2 →
+ ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G0,L1❫ ⊢ ⓓ[p]W1.ⓐU1.T1 ➡[h,0] T & ❪G0,L2❫ ⊢ ⓓ[p]W2.ⓐU2.T2 ➡[h,0] T.