apply Finset.union_subset_left_right
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ∪ psi.freeVarSet ⊆
    (Formula.open j (free_ z) phi).freeVarSet ∪ (Formula.open j (free_ z) psi).freeVarSet
case h1
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet

case h2
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet