intro u w_α_u
case mpr
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✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
⊢ ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
case mpr
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✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ evaluate M u (⌈⌈δ⌉⌉φ)