| ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV
| ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
| ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV
| ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &