simp only [subst_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
⊢ w = v → (evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ)