Implementation of McBride's "First-order unification by structural recursion" in Agda.