simp only [Formula.lc_at] at h1
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j (forall_ x phi)
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi