feat(data/vector2): add lemma map_id (#4799)
`map_id` proves that a vector is unchanged when mapped under the `id` function. This is similar to `list.map_id`. This lemma was marked with the `simp` attribute to make it available to the simplifier.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
