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

case not_
zs : List String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j a✝.not_
⊢ openList j (List.map free_ zs) a✝.not_ = a✝.not_

case imp_
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (j : ℕ), lc_at j a✝¹ → openList j (List.map free_ zs) a✝¹ = a✝¹
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (a✝¹.imp_ a✝)
⊢ openList j (List.map free_ zs) (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case forall_
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (forall_ a✝¹ a✝)
⊢ openList j (List.map free_ zs) (forall_ a✝¹ a✝) = forall_ a✝¹ a✝