proposition: Lemma mk_tou_irreflexive A (ll : list (list A)) (ND: NoDup (concat ll)) : irreflexive (mk_tou ll).
proof: Proof. red; unfold mk_tou; ins; desf. eapply total_order_from_list_irreflexive in H0; eauto using NoDup_concatD. Qed.
imports: HahnBase HahnList HahnRelationsBasic