MAYBE
ignored inputs:
(COMMENT alpha reduction rule of the lambda calculus )

NRS:
   [ (0): b#X |- (lam [a][]X) -> (lam [b][(a b)]X) ]
Check confluence by orthogonality
not abstract skeleton preserving
result: MAYBE
time: 0 msec.