- | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ J = Cast)
- | (⦃h, L⦄ ⊢ V1 ➡[g] U2 ∧ J = Cast)
- | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 &
- ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 &
+ | (⦃G, L⦄ ⊢ U1 ➡[h, g] U2 ∧ J = Cast)
+ | (⦃G, L⦄ ⊢ V1 ➡[h, g] U2 ∧ J = Cast)
+ | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 &
+ ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[h, g] T2 &