When going under a binder, a term must be converted twice, as explained in the

When going under a binder, a term must be converted twice, as explained in the
previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.