proposition: Lemma mk_po_insert : forall A init ll1 (l1: list A) a l2 ll2 x y, mk_po init (ll1 ++ (l1 ++ l2) :: ll2) x y -> mk_po init (ll1 ++ (l1 ++ a :: l2) :: ll2) x y.
proof: Proof. unfold mk_po; ins; desf; eauto using mk_tou_insert. rewrite concat_app, concat_cons, <- app_assoc, !in_app_iff in *. ins; desf; eauto 8. Qed.
imports: HahnBase HahnList HahnRelationsBasic