proposition: Lemma mk_tou_helper A (ll : list (list A)) (ND: NoDup (concat ll)) : forall a b (IMM: immediate (mk_tou ll) a b), (forall x, mk_tou ll a x <-> x = b \/ mk_tou ll b x) /\ (forall x, mk_tou ll x b <-> x = a \/ mk_tou ll x a).
proof: Proof. unfold mk_tou, immediate; ins; desf. edestruct total_order_from_list_helper with (l:=l); eauto using NoDup_concatD. split; ins; eauto 8. clear IMM0; assert (X:=IMM1); apply total_order_from_list_in in X; desc. intuition; desf; eauto. assert (l0 = l); [|by subst; rewrite H in *; desf; eauto]. by eauto using NoDup_concat_simpl, total_order_from_list_in1. eexists; split; eauto. assert (l0 = l); [|by subst; rewrite H in *; desf; eauto]. by eauto using NoDup_concat_simpl, total_order_from_list_in1. destruct (classic (x = a)); eauto. right; eexists; split; eauto. assert (l0 = l); [|by subst; rewrite H0 in *; desf; eauto]. by eauto using NoDup_concat_simpl, total_order_from_list_in2. eexists; split; eauto. assert (l0 = l); [|by subst; rewrite H0 in *; desf; eauto]. by eauto using NoDup_concat_simpl, total_order_from_list_in2. Qed.
imports: HahnBase HahnList HahnRelationsBasic