proposition: Lemma total_order_from_list_swap : forall A (l1: list A) a b l2 x y, total_order_from_list (l1 ++ a :: b :: l2) x y -> (x = a -> b = y -> False) -> total_order_from_list (l1 ++ b :: a :: l2) x y.
proof: Proof. ins; rewrite total_order_from_list_app, !total_order_from_list_cons in *; ins; intuition; desf; exfalso; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic