t_fold already iters on the subterms of a term, so calling t_fold on a
subterm actually iters over grandchildren of the term, which may well be
under a quantifier. So t_fold should be called on the term itself.

This explains why the transformation was trying to create declarations with
unbounded variables.