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