simp only [repl_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
⊢ w = v → (evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ)