proposition: Lemma nodup_prefixes a : NoDup (prefixes a).
proof: Proof. assert (X := sorted_prefixes a); ins; desf. eapply NoDup_StronglySorted; try apply TOT; auto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt