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