proposition: Lemma list_before_irr l : irreflexive (list_before l).
proof: Proof. unfold list_before; red; ins; desf. rewrite nodup_app, nodup_cons in *; desf; eauto with hahn. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic