Add a [map_ext_in] lemma to List.v.

Slightly broader version of the existing [map_ext]: two [map] expressions
are equal if their respective functions agree on all arguments that are
in the list being mapped.