- ∀n1,V1. ❪G0,L0❫ ⊢ V0 ➡[n1,h] V1 → V0 ≛ V1 →
- ∀n2,V2. ❪G0,L0❫ ⊢ V0 ➡[n2,h] V2 → V0 ≛ V2 →
- ∀T1. ❪G0,L0❫ ⊢ T0 ➡[n1,h] T1 → T0 ≛ T1 →
- ∀T2. ❪G0,L0❫ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 →
- ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 →
- ∃∃T. ❪G0,L1❫ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⓝV1.T1 ≛ T & ❪G0,L2❫ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2 ≛ T.
+ ∀n1,V1. ❪G0,L0❫ ⊢ V0 ➡[h,n1] V1 → V0 ≛ V1 →
+ ∀n2,V2. ❪G0,L0❫ ⊢ V0 ➡[h,n2] V2 → V0 ≛ V2 →
+ ∀T1. ❪G0,L0❫ ⊢ T0 ➡[h,n1] T1 → T0 ≛ T1 →
+ ∀T2. ❪G0,L0❫ ⊢ T0 ➡[h,n2] T2 → T0 ≛ T2 →
+ ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G0,L1❫ ⊢ ⓝV1.T1 ➡[h,n2-n1] T & ⓝV1.T1 ≛ T & ❪G0,L2❫ ⊢ ⓝV2.T2 ➡[h,n1-n2] T & ⓝV2.T2 ≛ T.