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