simp only [Formula.openList]
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (forall_ x phi)).freeVarSet ⊆
    (forall_ x phi).freeVarSet ∪ (List.map free_ zs).toFinset
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (forall_ x (Formula.openList (j + 1) (List.map free_ zs) phi)).freeVarSet ⊆
    (forall_ x phi).freeVarSet ∪ (List.map free_ zs).toFinset