case and φ1 φ2 =>
  have IH1 := repl_in_model_sat_iff x ψ φ1 M w
  have IH2 := repl_in_model_sat_iff x ψ φ2 M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  rw [IH1, IH2]
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
no goals