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

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