proposition: Lemma nodup_eq_one A (x : A) l : NoDup l -> In x l -> (forall y (IN: In y l), y = x) -> l = x :: nil.
proof: Proof. destruct l; ins; f_equal; eauto. inv H; desf; clear H H5; induction l; ins; desf; case H4; eauto using eq_sym. rewrite IHl in H0; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation