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 :)
Interested readers should check out Agda and Theorems for free!