simp only [evaluatePoint, modelCanSemImplyForm] at *
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : (repl_in_model x ψ M, w)⊨φ1 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2