simp at φ_in
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
φ_in : φ ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)
w_φ : evaluate M w φ
⊢ evaluate M w (⌈γ⌉ψ)
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
φ_in : ∃ a ∈ allTP γ, Con (Xset γ a ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)