rw [disEval]
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f