case not_ phi phi_ih =>
  simp only [occursFreeIn] at h1
  simp only [Holds]
  congr! 1
  exact phi_ih V V' h1
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi.not_ → V v = V' v
⊢ Holds D I V phi.not_ ↔ Holds D I V' phi.not_
no goals