proposition: Lemma mk_po_immediateD A init ll (a b : A) : immediate (mk_po init ll) a b -> ~ In a init -> exists ll1 l1 l2 ll2, ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2.
proof: Proof. ins; eapply mk_tou_immediateD; unfold immediate, mk_po in *; desf; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic