proposition: Lemma mk_po_irreflexive A (init : list A) ll (ND: NoDup (init ++ concat ll)) x : mk_po init ll x x -> False.
proof: Proof. unfold mk_po; ins; rewrite nodup_app in *; desf; eauto. eapply mk_tou_irreflexive; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic