proposition: Lemma mk_po_reorder init ll1 l1 a b l2 ll2 : NoDup (init ++ concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) -> reorder (mk_po init (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) a b ≡ mk_po init (ll1 ++ (l1 ++ b :: a :: l2) :: ll2).
proof: Proof. Proof using. unfold reorder; split; red; ins; desf; eauto using mk_po_swap, mk_po_trivial. destruct (classic (x = b /\ y = a)); eauto 8 using mk_po_swap, mk_po_trivial. left; split; ins; desf; eauto using mk_po_swap, mk_po_trivial. intro; desf; eauto 8 using mk_po_trans, mk_po_trivial, mk_po_irreflexive. Qed.
imports: HahnBase HahnList HahnRelationsBasic