proposition: Lemma mk_po_trans A init ll (D: NoDup (init ++ concat ll)) (x y z : A) : mk_po init ll x y -> mk_po init ll y z -> mk_po init ll x z.
proof: Proof. unfold mk_po; ins; rewrite nodup_app in *; desf; eauto using mk_tou_trans, mk_tou_in2. exfalso; eauto using mk_tou_in1, mk_tou_in2. Qed.
imports: HahnBase HahnList HahnRelationsBasic