- | (⦃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] 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 &