proposition: Lemma remove_red_included : forall e l, mem eq_A e l -> mem eq_A e (remove_red l).
proof: Proof. fix remove_red_included 2. intros x l; case l; clear l. intro H; exact H. intros a l; simpl; generalize (mem_bool_ok _ _ eq_bool_ok a l); case (mem_bool eq_bool a l). intros a_in_l x_in_al; case x_in_al; clear x_in_al. intro x_eq_a; apply remove_red_included. apply (mem_eq_mem eq_proof a x l (equiv_sym _ _ eq_proof _ _ x_eq_a) a_in_l). intro x_in_l; exact (remove_red_included x l x_in_l). intros _ x_in_al; case x_in_al; clear x_in_al. intro x_eq_a; left; exact x_eq_a. intro x_in_l; right; exact (remove_red_included x l x_in_l). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)