proposition: Lemma list_before_app l l' x y : list_before (l ++ l') x y <-> NoDup (l ++ l') /\ (list_before l x y \/ list_before l' x y \/ In x l /\ In y l').
proof: Proof. unfold list_before; intuition; desf. all: repeat (rewrite <- app_assoc in *; ins); eauto. 2: by eexists (_ ++ _), _, _; rewrite app_assoc. 2: apply in_split in H; desf; apply in_split in H2; desf. 2: exists l1, (l2 ++ l0), l3; repeat (rewrite <- app_assoc; ins). rewrite nodup_app in *; desf. apply list_app_eq_app in H1; desf; eauto 8. destruct lr; ins; desf; rewrite ?app_nil_r in *. right; left; split; eauto; exists nil; ins; eauto. apply list_app_eq_app in H1; desf; eauto 8 with hahn. destruct lr0; ins; desf; rewrite ?app_nil_r in *; eauto 8 with hahn. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic