proposition: Lemma list_before_hd l x y : list_before (x :: l) x y <-> ~ In x l /\ In y l /\ NoDup l.
proof: Proof. rewrite list_before_cons; unfold list_before; intuition; desf; auto with hahn. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic