subst w_is_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_is_v : w = v
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IHφ : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ