proposition: Lemma without_red_permut : forall l1 l2, without_red l1 -> LP.permut l1 l2 -> without_red l2.
proof: Proof. unfold without_red; fix without_red_permut 1. intros l1; case l1; clear l1. intros l2 _ P; rewrite (permut_nil (permut_sym P)); reflexivity. intros a1 l1 l2; simpl. generalize (mem_bool_ok _ _ eq_bool_ok a1 l1); case (mem_bool eq_bool a1 l1). intros; discriminate. intros a1_not_in_l1 wr1 P;assert (a1_in_l2 := cons_permut_mem (Relation_Definitions.equiv_refl _ _ eq_proof a1) P). case (mem_split_set _ _ eq_bool_ok _ _ a1_in_l2); intros a1' M; case M; clear M. intros l2' M; case M; clear M. intros l2'' M; case M; clear M. intros a1_eq_a1' M; case M; clear M. intros H _; subst l2. rewrite <- permut_cons_inside in P; [idtac | exact a1_eq_a1']. apply add_prf. apply (without_red_permut l1); trivial. rewrite <- (mem_permut_mem a1' P). intro a1_in_l1; apply a1_not_in_l1. apply (mem_eq_mem eq_proof a1' a1 l1 (equiv_sym _ _ eq_proof _ _ a1_eq_a1') a1_in_l1). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)