proposition: Lemma mk_po_immediate A init ll1 l1 l2 ll2 (a b : A) : NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) -> immediate (mk_po init (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) a b.
proof: Proof. rewrite nodup_app; unfold mk_po; ins; desc. unfold mk_po; split; ins; desf; eauto 7 using in_concat, in_or_app, in_eq, in_cons, mk_tou_in1, mk_tou_in2. right; apply mk_tou_immediate; eauto. eapply mk_tou_immediate; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic