Add lemma `later_map_Next`.

This is more or less the definition, but (1) it does not expose later_car and (2) it is useful when rewriting.