proposition: Lemma list_before_trans l x y z : list_before l x y -> list_before l y z -> list_before l x z.
proof: Proof. unfold list_before; ins; desf; split; ins. clear H0; rename H1 into X. repeat first [rewrite nodup_app in * | rewrite nodup_cons in *]; desf. apply list_app_eq_app in X; desf. destruct lr; ins; desf; try solve [exfalso; eauto with hahn]. by rewrite H7; eexists l0, (lr ++ y :: l2), l3; ins; rewrite <- app_assoc. destruct lr; ins; desf; exfalso; eauto with hahn. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic