First-occurrence indices under injective maps on a list

List.idxOf_map_injOn preserves the first occurrence of a member when the map is injective only on the elements that occur. Repeated elements are allowed, and the map may behave arbitrarily outside the list. Membership of the searched value is required. The proof is relocated unchanged from CNF compaction's relabeling API.

theorem List.idxOf_map_injOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (l : List V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ l}) {v : V} (hv : v ∈ l) : idxOf (f v) (map f l) = idxOf v l

An injection on occurring elements preserves the first-occurrence index of a member.