apply phi_ih
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) phi) ↔ Formula.lc_at (j + zs.length) phi
no goals