simp only [Formula.openList]
phi psi : 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
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (phi.imp_ psi)) ↔ Formula.lc_at (j + zs.length) (phi.imp_ psi)
phi psi : 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
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)) ↔
    Formula.lc_at (j + zs.length) (phi.imp_ psi)