Beta-expansion was avoided as soon as one argument was flexible.

This lead to a different behaviour in the following two unification problems:

   (\lambda_.?) ? =?= T         vs               ? ? =?= T
     or, equivalently
        ?[?] =?= T

The fix is very easy: we always perform beta-expansion and delifting will
take care of ignoring the flexible "arguments", both during beta-expansion
and during the unification that follows.