induction F generalizing j
j : ℕ
zs : List String
F : Formula
⊢ (Formula.openList j (List.map free_ zs) F).freeVarSet ⊆ F.freeVarSet ∪ (List.map free_ zs).toFinset
case pred_
zs : List String
a✝¹ : String
a✝ : List Var
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝)).freeVarSet ⊆
    (pred_ a✝¹ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case not_
zs : List String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) a✝.not_).freeVarSet ⊆ a✝.not_.freeVarSet ∪ (List.map free_ zs).toFinset

case imp_
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝¹).freeVarSet ⊆ a✝¹.freeVarSet ∪ (List.map free_ zs).toFinset
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝)).freeVarSet ⊆
    (a✝¹.imp_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case forall_
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝)).freeVarSet ⊆
    (forall_ a✝¹ a✝).freeVarSet ∪ (List.map free_ zs).toFinset