proposition: Lemma mk_tou_trivial A ll1 l1 l2 ll2 (a b : A) : mk_tou (ll1 ++ (l1 ++ a :: b :: l2) :: ll2) a b.
proof: Proof. by eexists; split; eauto using in_or_app, in_eq; eexists _, nil, _. Qed.
imports: HahnBase HahnList HahnRelationsBasic