Dense first-occurrence names under one-point identification

On occurring names, updating the dense name of b to that of a has exactly the kernel of updating the original identity at b to a. The list may repeat elements; neither selected point is required to occur. The explicit membership hypotheses apply only to the compared names. This original identity supports actual incidence vertex-identification transport.

theorem List.idxOf_update_id_eq_iff {α : Type u_1} [DecidableEq α] (l : List α) (a b x y : α) (hx : x ∈ l) (hy : y ∈ l) : Function.update id (idxOf b l) (idxOf a l) (idxOf x l) = Function.update id (idxOf b l) (idxOf a l) (idxOf y l) ↔ Function.update id b a x = Function.update id b a y

Dense and original one-point identifications equate precisely the same occurring names. Repeated elements and arbitrary selected names outside the list are permitted.