Unification under a mixed prefix

http://www.lix.polytechnique.fr/~dale/papers/jsc92.pdf

Relevant to logic programming, theorem proving, and dependent pattern matching as, e.g., found in the highly-voted "Why dependent types matter" (#74).