exact phi_ih
case h1
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 ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
no goals