proposition: Lemma included_remove_red : forall e l, mem eq_A e (remove_red l) -> mem eq_A e l.
proof: Proof. fix included_remove_red 2. intros x l; case l; clear l. intro H; exact H. intros a l; simpl; case (mem_bool eq_bool a l). intros x_in_rl; right; exact (included_remove_red x l x_in_rl). intro x_in_arl; simpl in x_in_arl; case x_in_arl; clear x_in_arl. intro x_eq_a; left; exact x_eq_a. intro x_in_rl; right; exact (included_remove_red x l x_in_rl). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)