∀ {α : 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)