induction F generalizing j zs
F : Formula
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) F) ↔ Formula.lc_at (j + zs.length) F
case pred_
a✝¹ : String
a✝ : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝)) ↔ Formula.lc_at (j + zs.length) (pred_ a✝¹ a✝)

case not_
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝.not_) ↔ Formula.lc_at (j + zs.length) a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝¹) ↔ Formula.lc_at (j + zs.length) a✝¹
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝)) ↔ Formula.lc_at (j + zs.length) (a✝¹.imp_ a✝)

case forall_
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝¹ a✝)