The problem of unification in this lambda-calculus is, of course,
undecidable, but a pre-unification algorithm in the style of
Huet exists. We describe this algorithm and show that, perhaps
somewhat surprisingly, a similar algorithm does not exist for the
multiplicative-exponential fragment.