proposition: Lemma nodup_rev A (l : list A) : NoDup (rev l) <-> NoDup l.
proof: Proof. induction l; ins. rewrite nodup_app, !nodup_cons, IHl, disjoint_rev_l, disjoint_one_r; intuition. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation