proposition: Lemma mk_tou_trans A (ll : list (list A)) (ND: NoDup (concat ll)) x y z : mk_tou ll x y -> mk_tou ll y z -> mk_tou ll x z.
proof: Proof. unfold mk_tou; ins; desf. assert (l0 = l); subst. by eapply NoDup_concat_simpl; eauto using total_order_from_list_in1, total_order_from_list_in2. apply in_split_perm in H0; desc. rewrite H0, concat_cons, nodup_app in ND; desc. eauto using total_order_from_list_trans. Qed.
imports: HahnBase HahnList HahnRelationsBasic