- | (⦃G, L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
- | (⦃G, L⦄ ⊢ V1 ⬈[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 &
+ | (⦃G,L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
+ | (⦃G,L⦄ ⊢ V1 ⬈[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 &