-- This definition uses narrowing...
rev [] []     = True
rev zs (x:xs) | rx ++ [x] == zs & rev rx xs
              = True                              where rx free
-- ...so that the evaluation of (rev [1,2] xs) has a 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
-- ...so that the evaluation of (revR [1,2] xs) has an infinite search space