YES
ignored inputs:
(COMMENT eta reduction rule of the lambda calculus )

NRS:
   [ (0): a#X |- (lam [a](app <[]X,a>)) -> []X ]
Check confluence by strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   { a#X_1 |- < []X_1 <= (lam [a](app <[]X_1,a>)) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (lam [b](app <[]X_1,b>)) => []X_1 > }
all BCPs are strongly closed
result: YES
time: 1 msec.