| ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = ↓cV
| ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
| ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = ↓cV
| ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &