proposition: Lemma total_order_from_list_app : forall A (l1 l2: list A) x y, total_order_from_list (l1 ++ l2) x y <-> In x l1 /\ In y l2 \/ total_order_from_list l1 x y \/ total_order_from_list l2 x y.
proof: Proof. induction l1; ins. intuition; eauto. by unfold total_order_from_list in *; desf; destruct l1; ins. rewrite !total_order_from_list_cons, IHl1, in_app_iff; clear; intuition. Qed.
imports: HahnBase HahnList HahnRelationsBasic