proposition: Lemma mk_po_helper A init (ll : list (list A)) (ND: NoDup (init ++ concat ll)) : forall a (NI: ~ In a init) b (IMM: immediate (mk_po init ll) a b), (forall x, mk_po init ll a x <-> x = b \/ mk_po init ll b x) /\ (forall x, mk_po init ll x b <-> x = a \/ mk_po init ll x a).
proof: Proof. unfold mk_po, immediate; ins; desf. rewrite nodup_app in ND; desc. apply mk_tou_helper with (a:=a) (b:=b) in ND0; desc. 2: by split; ins; eauto. clear IMM0; split; ins. by rewrite ND0; intuition; exfalso; eauto using mk_tou_in2. by rewrite ND2; intuition; eauto using mk_tou_in1, mk_tou_in2. Qed.
imports: HahnBase HahnList HahnRelationsBasic