proposition: Lemma without_red_remove : forall e l1 l2, without_red (l1 ++ e :: l2) -> without_red (l1 ++ l2).
proof: Proof. unfold without_red; fix without_red_remove 2. intros e l1 l2; case l1; clear l1; simpl. case (mem_bool eq_bool e l2); [intro H; discriminate | trivial]. intros e1 l1; generalize (mem_bool_ok _ _ eq_bool_ok e1 (l1 ++ e :: l2)). case (mem_bool eq_bool e1 (l1 ++ e :: l2)). intros; discriminate. intros e1_not_mem_l Wl. generalize (mem_bool_ok _ _ eq_bool_ok e1 (l1 ++ l2)). case (mem_bool eq_bool e1 (l1 ++ l2)). intro e1_mem_l'; apply False_rect; apply e1_not_mem_l; apply mem_insert; trivial. intro; apply (without_red_remove e l1 l2); trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)