- | (❪G,L❫ ⊢ U1 ➡[h] U2 ∧ I = Cast)
- | ∃∃p,V2,W1,W2,T1,T2. ❪G,L❫ ⊢ V1 ➡[h] V2 & ❪G,L❫ ⊢ W1 ➡[h] W2 &
- ❪G,L.ⓛW1❫ ⊢ T1 ➡[h] T2 & U1 = ⓛ[p]W1.T1 &
+ | (❪G,L❫ ⊢ U1 ➡[h,0] U2 ∧ I = Cast)
+ | ∃∃p,V2,W1,W2,T1,T2. ❪G,L❫ ⊢ V1 ➡[h,0] V2 & ❪G,L❫ ⊢ W1 ➡[h,0] W2 &
+ ❪G,L.ⓛW1❫ ⊢ T1 ➡[h,0] T2 & U1 = ⓛ[p]W1.T1 &