proposition: Lemma add_prf : forall e l1 l2, without_red (l1 ++ l2) -> ~mem eq_A e (l1 ++ l2) -> without_red (l1 ++ e :: l2).
proof: Proof. unfold without_red; fix add_prf 2. intros e l1 l2; case l1; clear l1; simpl. intros wr12 e_not_in_l1_l2; generalize (mem_bool_ok _ _ eq_bool_ok e l2); case (mem_bool eq_bool e l2). intro e_in_l2; absurd (mem eq_A e l2); assumption. intros _; exact wr12. intros e1 l1 wr12 e_not_in_l1_l2; generalize (mem_bool_ok _ _ eq_bool_ok e1 (l1 ++ e :: l2)). case (mem_bool eq_bool e1 (l1 ++ e :: l2)). intro e1_in_l1_l2; absurd (mem eq_A e1 (l1 ++ l2)). apply (without_red_not_in e1 nil (l1 ++ l2)); trivial. apply diff_mem_remove with e; trivial; intro; apply e_not_in_l1_l2; subst; left; symmetry; trivial. intros _; apply add_prf. apply (without_red_remove e1 nil (l1 ++ l2)); trivial. intro; apply e_not_in_l1_l2; right; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)