simp [evaluatePoint, modelCanSemImplyForm] at *
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
IH2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
IH2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ∧ evaluate M w (repl_in_F x ψ φ2) ↔
    evaluate (repl_in_model x ψ M) w φ1 ∧ evaluate (repl_in_model x ψ M) w φ2