proposition: Lemma mk_tou_remove : forall A ll1 (l1: list A) a l2 ll2 x y, mk_tou (ll1 ++ (l1 ++ a :: l2) :: ll2) x y -> x <> a -> y <> a -> mk_tou (ll1 ++ (l1 ++ l2) :: ll2) x y.
proof: Proof. unfold mk_tou; ins; desf; rewrite in_app_iff in *; ins; desf; eauto 8 using in_or_app, in_eq, in_cons, total_order_from_list_remove. Qed.
imports: HahnBase HahnList HahnRelationsBasic