# is this an example of nominal unification?

I am thinking that is the following a problem solved by nominal unification.

$\lambda a.X = \lambda b.\lambda c.c$

where we find $X$. The answer is obvious.

The reason is that it seems in nominal unification $X$ always will be an atom, not a function such as $\lambda c.c$. The theory seems works fine with this input, just did not saw any example similar to this one.

Sure, these unify under nominal unification. You get a unifier like $X = (b\ a)\bullet\lambda c.c$ which simplifies to $X = \lambda c.c$. Figures 1 and 3 of Nominal Unification describe the relevant details of the algorithm. In particular the transitions will be $\approx?$-abstraction-2 and $\approx?$-variable followed by $\#?$-abstraction-2 and $\#?$-atom.