∀ {α : Type u} {α' : Type u'} [inst : DecidableEq α] [inst_1 : DecidableEq α'] {β : Type v} (l : List ((_ : α) × β))
  {f : α → α'},
  Function.Injective f → ∀ (a : α), List.dlookup (f a) (List.map (Sigma.map f fun x => id) l) = List.dlookup a l