Prove [map_ext] using [map_ext_in].

Since [map_ext_in] is more general, no need to have the same proof twice.