proposition: Lemma without_red_remove_red : forall l, without_red (remove_red l).
proof: Proof. unfold without_red; fix without_red_remove_red 1. intro l; case l; clear l. reflexivity. intros a l; simpl. generalize (mem_bool_ok _ _ eq_bool_ok a l); case (mem_bool eq_bool a l). intro a_in_l; apply without_red_remove_red. intro a_not_in_l; simpl; generalize (mem_bool_ok _ _ eq_bool_ok a (remove_red l)). case (mem_bool eq_bool a (remove_red l)). intro a_in_rl; absurd (mem eq_A a l). assumption. apply included_remove_red; trivial. intro a_not_in_rl; apply without_red_remove_red. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)