case and φ1 φ2 =>
  have IH1 := substitutionLemma σ φ1 M w
  have IH2 := substitutionLemma σ φ2 M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  rw [IH1, IH2]
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
no goals