intro v v_αδ_w
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✝), relateSeq M (α :: δ) w v → evaluate M 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 : relateSeq M (α :: δ) w v
⊢ evaluate M v φ