∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-m12] T & ❪G0,L2❫ ⊢ T2 ➡*[h,m12-(m21+m22)]T
∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-m12] T & ❪G0,L2❫ ⊢ T2 ➡*[h,m12-(m21+m22)]T