case forall_ _ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.lc_at]
  simp only [phi_ih]
  have s1 : j + 1 + List.length zs = j + List.length zs + 1
  linarith;
  simp only [s1]
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝ phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
no goals