case atom_prop c =>
  simp [evaluatePoint, modelCanSemImplyForm, evaluate, repl_in_model]
  aesop
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·c) ↔ (repl_in_model x ψ M, w)⊨·c
no goals