case neg φ =>
  have IH := repl_in_model_sat_iff x ψ φ M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  tauto
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨repl_in_F x ψ (~φ) ↔ (repl_in_model x ψ M, w)⊨(~φ)
no goals