MAYBE
ignored inputs:
(COMMENT Example 19 of [ SKAT15 , doi:10.4230/LIPIcs.RTA.2015.301 ] )

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