case test φ =>
  have IHφ := repl_in_model_sat_iff x ψ φ M v
  simp only [repl_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
  intro w_is_v
  subst w_is_v
  exact IHφ
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
no goals