coq/coq — pull request #45 by zeldovich (2014-11-09 17:02:41+00:00)
Title: 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.