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