proposition: Lemma list_before_mid_r l l' x y : list_before (l ++ y :: l') x y <-> NoDup (l ++ y :: l') /\ In x l.
proof: Proof. rewrite list_before_app, list_before_cons; split; ins; desf; splits; ins; eauto using list_before_in1. edestruct H0; ins; eauto using list_before_in2. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic