MAYBE
ignored inputs:
(COMMENT Example 4.3 of [ Ayala-Lincon et al. , LSFA 2015 ] )

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