case test φ =>
  have IHφ := substitutionLemma σ φ M v
  simp only [subst_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
  intro w_is_v
  subst w_is_v
  exact IHφ
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
no goals