proposition: Lemma NoDup_StronglySorted A (r: relation A) (IRR: irreflexive r) l (SS: StronglySorted r l): NoDup l.
proof: Proof. induction l; ins. apply StronglySorted_inv in SS; desc. rewrite Forall_forall in *. constructor; eauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid