apply Finset.union_subset_left_right_diff
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet ⊆
    t.freeVarSet ∪ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}
case h1
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}

case h2
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}