proposition: Lemma included_filter_aux : forall P_bool e l, more_list.mem eq_A e (filter_aux P_bool l) -> more_list.mem eq_A e l.
proof: Proof. intros P_bool x l; functional induction (filter_aux P_bool l) as [ | H1 e l H2 P_e IH | H1 e l H2 not_P_e IH ]. trivial. intros [x_eq_e | x_in_fl]; [left | right; apply IH]; trivial. intros x_in_fl; right; apply IH; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)