rcases v_αδ_w with ⟨u, w_α_u, u_δ_v⟩
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : ∃ u, relate M α w u ∧ relateSeq M δ u v
⊢ evaluate M v φ
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ