proposition: Lemma filter_2_list : forall (P : elt -> Prop) P_dec l e, In e (filter_aux P P_dec l) -> In e l /\ P e.
proof: Proof. intros P P_dec l; induction l as [ | e' l]. contradiction. intros e; simpl; destruct (P_dec e') as [ Pe' | not_Pe' ]. intros [e_eq_e' | e_in_fltl]. subst; split; trivial; left; trivial. generalize (IHl _ e_in_fltl); intros [e_in_l Pe]; split; trivial; right; trivial. intro e_in_fltl; generalize (IHl _ e_in_fltl); intros [e_in_l Pe]; split; trivial; right; trivial. Qed.
imports: List more_list list_permut Arith