intro w_is_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 φ)
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
w_is_v : w = v
⊢ evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ