simp [evaluatePoint, modelCanSemImplyForm, evaluate, repl_in_model]
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·c) ↔ (repl_in_model x ψ M, w)⊨·c
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ evaluate M w (if c = x then ψ else ·c) ↔ if c = x then evaluate { val := M.val, Rel := M.Rel } w ψ else M.val w c