A new unification algorithm is introduced, which (unlike previous algorithms for unification in λ-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
proofsearch algorithms to second-order logic, making possible for example a straighforward treatment of McCarthy's circumscription
schema.