proposition: Lemma filter_2_list : forall (P_bool : A -> bool) l e (P_compat : forall e e', eq_A e e' -> (P_bool e = P_bool e')), more_list.mem eq_A e (filter_aux P_bool l) -> more_list.mem eq_A e l /\ P_bool e = true.
proof: Proof. intros P_bool l e P_compat H; functional induction (filter_aux P_bool l) as [ | H1 e' l H2 P_e' IH | H1 e' l H2 not_P_e IH ]. contradiction. destruct H as [e_eq_e' | e_in_fl]; split. left; trivial. rewrite (P_compat e e'); trivial. right; apply (proj1 (IH e_in_fl)). apply (proj2 (IH e_in_fl)). split; [right | idtac]; destruct (IH H); trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)