Abstract of Unification in Lambda Calculus with If-then-else:

A new unification algorithm is introduced, which (unlike previous algorithms for unification in lambda-calculus)shares the pleasant properties of first-order unification.  Proofs of these properties are given, in particular uniqueness of the answer and the most-general-unifier property. This unification algorithm can be used to generalize first-order proof-search algorithms to second-order logic, making possible for example a straighforward treatment of McCarthy's circumscription schema.