proposition: Lemma without_red_not_in : forall e l1 l2, without_red (l1 ++ e :: l2) -> ~mem eq_A e (l1 ++ l2).
proof: Proof. unfold without_red; fix without_red_not_in 2. intros e l1 l2; case l1; clear l1; simpl. generalize (mem_bool_ok _ _ eq_bool_ok e l2); case (mem_bool eq_bool e l2). intros _ H _; discriminate. intros H _; exact H. intros e1 l1; generalize (mem_bool_ok _ _ eq_bool_ok e1 (l1 ++ e :: l2)); case (mem_bool eq_bool e1 (l1 ++ e :: l2)). intros _ H _; discriminate. intros e1_not_in_l1_e_l2 wr [e_eq_e1 | e_mem_l1l2]; apply e1_not_in_l1_e_l2. rewrite <- mem_or_app; right; left; symmetry; assumption. apply False_rect; apply (without_red_not_in e l1 l2 wr e_mem_l1l2). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)