proposition: Lemma filter_1_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 l -> P_bool e = true -> more_list.mem eq_A e (filter_aux P_bool l).
proof: Proof. intros P_bool l e P_compat e_in_l P_e; 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 e_in_l as [e_eq_e' | e_in_l]; [left | right; apply IH]; trivial. simpl in e_in_l; destruct e_in_l as [e_eq_e' | e_in_l]. rewrite (P_compat e e') in P_e; trivial; rewrite P_e in not_P_e; discriminate. apply IH; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)