have : evaluate M w ψ := by tauto
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ (M, w)⊨φ
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w ψ
⊢ (M, w)⊨φ