proposition: Lemma list_before_cons a l x y : list_before (a :: l) x y <-> a = x /\ ~ In x l /\ In y l /\ NoDup l \/ ~ In a l /\ list_before l x y.
proof: Proof. rewrite list_before_app with (l := a :: nil) (l' := l); ins; rewrite nodup_cons in *. split; ins; desf; splits; eauto with hahn; try (edestruct list_before_singl; eassumption). red in H0; desf. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic