simp only [Formula.freeVarSet]
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ ((Formula.close j (free_ z) phi).imp_ (Formula.close j (free_ z) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet \ {free_ z}
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ∪ (Formula.close j (free_ z) psi).freeVarSet ⊆
    (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}