In other words, `foldr` (flipped about) takes a list to its Church encoding: since it just ‘replaces the constructors’ (`:` becomes `f`, `[]` becomes `z`), it doesn't lose any information from the list: if you can write a function by recursing on a list then you can write it using `foldr`.