-- This definition uses narrowing...
rev [] []     = True
rev zs (x:xs) | rx ++ [x] == zs & rev rx xs
              = True                              where rx free
-- Evaluation of (rev [1,2] xs)  --> finite search space

-- This definition uses residuation on the list concatenation...
revR [] []     = True
revR zs (x:xs) | ensureNotFree rx ++ [x] == zs & revR rx xs
               = True                              where rx free
-- Evaluation of (revR [1,2] xs)  --> INFINITE SEARCH SPACE!