proposition: Lemma list_before_filter_inv (f : A -> bool) l x y : list_before (filter f l) x y -> NoDup l -> list_before l x y.
proof: Proof. unfold list_before; ins; desf; splits; ins. apply filter_eq_app_cons in H1; desf. apply filter_eq_app_cons in H3; desf; eauto. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic