proposition: Lemma without_red_filter_aux : forall P_bool l, without_red l -> without_red (filter_aux P_bool l).
proof: Proof. unfold without_red; fix without_red_filter_aux 2. intros P_bool l; case l; clear l. intros _; reflexivity. simpl; intros a l. generalize (mem_bool_ok _ _ eq_bool_ok a l); case (mem_bool eq_bool a l). intros; discriminate. intros a_not_in_l Wl; case (P_bool a); simpl; rewrite (without_red_filter_aux P_bool l Wl). generalize (mem_bool_ok _ _ eq_bool_ok a (filter_aux P_bool l)); case (mem_bool eq_bool a (filter_aux P_bool l)). intro a_in_l; absurd (more_list.mem eq_A a l). assumption. apply included_filter_aux with P_bool; assumption. intros _; reflexivity. reflexivity. Defined.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)