simp only [Formula.freeVarSet]
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).imp_ (Formula.subst (free_ z) t psi)).freeVarSet ⊆
    t.freeVarSet ∪ (phi.imp_ psi).freeVarSet \ {free_ z}
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}