simp [evaluatePoint, modelCanSemImplyForm] at *
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (subst_in_F σ φ1) ↔ evaluate (subst_in_model σ M) w φ1
IH2 : evaluate M w (subst_in_F σ φ2) ↔ evaluate (subst_in_model σ M) w φ2
⊢ evaluate M w (subst_in_F σ φ1) ∧ evaluate M w (subst_in_F σ φ2) ↔
    evaluate (subst_in_model σ M) w φ1 ∧ evaluate (subst_in_model σ M) w φ2