> you can say that any `b` in the result list _must_ have come from applying the function to some `a` in the input list.
Morally correct... but consider the function `\f xs -> [undefined]`, which can be typed as `(a -> b) -> [a] -> [b]`. (Obviously it could be given other types as well.)
When discussing Haskell and theorems about its types it's common to simply ignore non-termination; if we don't ignore non-termination there's basically nothing we can say about Haskell programs at all.
Interested readers should check out Agda and Theorems for free!
Yeah that's a better one (which I think is discussed (or a similar one) in Theorems for free!), but the wording of OP weasels itself out of that being a problem.
> any `b` in the result list _must_ have come from applying the function to some `a` in the input list.
Since there exists no a in [], the quoted statement holds! I find that really beautiful :)
Morally correct... but consider the function `\f xs -> [undefined]`, which can be typed as `(a -> b) -> [a] -> [b]`. (Obviously it could be given other types as well.)