proposition: Lemma list_before_singl (a x y : A) : ~ list_before (a :: nil) x y.
proof: Proof. unfold list_before; intro; desf; destruct l1; ins; desf. destruct l2; ins; desf. destruct l1; ins; desf. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic