proposition: Lemma total_order_from_list_helper A (l : list A) (ND: NoDup l) : forall a b (IMM: immediate (total_order_from_list l) a b), (forall x, total_order_from_list l a x <-> x = b \/ total_order_from_list l b x) /\ (forall x, total_order_from_list l x b <-> x = a \/ total_order_from_list l x a).
proof: Proof. unfold immediate; ins; desf. red in IMM; desf. assert (l2 = nil); desf; ins. { destruct l2 as [|c ?]; ins; destruct (IMM0 c). eexists l1, nil, _; ins; eauto. eexists (l1 ++ a :: nil), _, _; rewrite <- app_assoc; ins; eauto. } rewrite nodup_app, !nodup_cons in *; desc. intuition; repeat first [rewrite total_order_from_list_app in * | rewrite total_order_from_list_cons in *]; ins; desf; eauto 8; try solve [exfalso; eauto using in_eq, in_cons, total_order_from_list_in1, total_order_from_list_in2]. Qed.
imports: HahnBase HahnList HahnRelationsBasic