MAYBE
ignored inputs:
(COMMENT eta expansion rule of the lambda calculus )

NRS:
   [ (0): a#X |- []X -> (lam [a](app <[]X,a>)) ]
variable conditions not hold
result: MAYBE
time: 0 msec.