simp only [Formula.subst]
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi.not_).freeVarSet
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).not_.freeVarSet