case not_ phi phi_ih =>
  simp only [Holds]
  congr! 1
  apply phi_ih
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi.not_)
no goals