rw [φ_eq_ψ] at this
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ