proposition: Lemma total_order_from_list_irreflexive A (l : list A) (ND: NoDup l) : irreflexive (total_order_from_list l).
proof: Proof. red; unfold total_order_from_list; ins; desf. induction l1; inv ND; ins; desf; eauto using in_or_app, in_eq. Qed.
imports: HahnBase HahnList HahnRelationsBasic