rw [conEval]
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ evaluate M w (Con (List.insert τ [~ψ]))
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ ∀ f ∈ List.insert τ [~ψ], evaluate M w f