induction δ generalizing w
W✝ : Type
M : KripkeModel W✝
w : W✝
δ : List Program
φ : Formula
⊢ evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
case nil
W✝ : Type
M : KripkeModel W✝
φ : Formula
w : W✝
⊢ evaluate M w (⌈⌈[]⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M [] w v → evaluate M v φ

case cons
W✝ : Type
M : KripkeModel W✝
φ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ {w : W✝}, evaluate M w (⌈⌈tail✝⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M tail✝ w v → evaluate M v φ
w : W✝
⊢ evaluate M w (⌈⌈head✝ :: tail✝⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M (head✝ :: tail✝) w v → evaluate M v φ