simp only [Formula.freeVarSet]
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (forall_ x (Formula.close (1 + j) (free_ z) phi)).freeVarSet ⊆ (forall_ x phi).freeVarSet \ {free_ z}
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close (1 + j) (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}