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

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