case not_ phi phi_ih =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  congr!
  exact phi_ih j h1
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi.not_
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
no goals