case neg φ =>
  have IH := substitutionLemma σ φ M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  tauto
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
no goals