pool optim, toward only head normal term added to the pool

[craff]

insert_t_node should use a stack to avoid creating node for partially applied function.

For instance, adding [add n p] to the pool also adds [add n] which is a lambda, hence trigger a cloture construction.

This cost is dominating "equiv" when computation are really needed, with probably a factor much greater that 2 (10 ?) to gain.