∀ {α : Type u} {xs : List ((_ : α) × α)} {a : (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs)}
  {a_1 : (List.map Sigma.snd xs).Nodup} {xs_1 : List ((_ : α) × α)}
  {a_2 : (List.map Sigma.fst xs_1).Perm (List.map Sigma.snd xs_1)} {a_3 : (List.map Sigma.snd xs_1).Nodup},
  Plausible.InjectiveFunction.mapToSelf xs a a_1 = Plausible.InjectiveFunction.mapToSelf xs_1 a_2 a_3 → xs = xs_1