proposition: Lemma list_before_neq l x y : list_before l x y -> x <> y.
proof: Proof. unfold list_before; red; ins; desf. rewrite nodup_app, nodup_cons in *; desf; eauto with hahn. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic