proposition: Lemma mk_tou_immediate A ll1 l1 l2 ll2 (a b : A) : NoDup (concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) -> immediate (mk_tou (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) a b.
proof: Proof. unfold mk_tou; red; ins; split; ins; desf. by eexists; split; eauto using in_or_app, in_eq; eexists _, nil, _. assert (l0 = l); subst. by eapply NoDup_concat_simpl; eauto using total_order_from_list_in1, total_order_from_list_in2. assert (l = l1 ++ a :: b :: l2); subst. by eapply NoDup_concat_simpl with (a:=a); eauto using in_or_app, in_eq, total_order_from_list_in1. rewrite concat_app, concat_cons in H. apply nodup_append_right, nodup_append_left in H. unfold total_order_from_list in *; desf. apply NoDup_eq_simpl in R3; desf. destruct l3; ins; desf. by rewrite R0, nodup_app, nodup_cons in *; desf; eauto using in_or_app, in_eq. replace (l0 ++ a :: a0 :: l3 ++ c :: l4) with ((l0 ++ a :: a0 :: l3) ++ c :: l4) in R0 by (rewrite <- app_assoc; done). eapply NoDup_eq_simpl in R0; desf. by rewrite !nodup_app, !nodup_cons in *; desf; eauto 8 using in_or_app, in_eq, in_cons. rewrite <- app_assoc; ins. Qed.
imports: HahnBase HahnList HahnRelationsBasic