proposition: Lemma mk_tou_immediateD A ll (a b : A) : immediate (mk_tou ll) a b -> exists ll1 l1 l2 ll2, ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2.
proof: Proof. unfold mk_tou, immediate; ins; desf. apply in_split in H; desf; red in H1; desf. destruct l3 as [|c ?]; ins; eauto. edestruct (H0 c); eexists; split; eauto using in_or_app, in_eq. by eexists _, nil, _; ins. by eexists (_ ++ _ :: nil), _, _; rewrite <- app_assoc; ins. Qed.
imports: HahnBase HahnList HahnRelationsBasic