proposition: Lemma without_red_permut : forall l1 l2, without_red l1 -> LP.list_permut l1 l2 -> without_red l2.
proof: Proof. intro l1; induction l1 as [ | e1 l1]. intros l2 _ P; rewrite (LP.list_permut_nil (LP.list_permut_sym P)); simpl; trivial. intros l2 wr1 P; assert (e1_in_l2 : In e1 l2). apply LP.in_permut_in with (e1 :: l1); trivial; left; trivial. generalize (split_list_app_cons eq_elt_dec _ _ e1_in_l2). simpl; destruct (split_list eq_elt_dec l2 e1) as [l2' l2'']; clear e1_in_l2. intro; subst; apply without_red_add. apply IHl1. apply (without_red_remove e1 nil l1); trivial. apply LP.list_permut_remove_hd with e1; trivial. intro H; simpl in wr1; destruct (In_dec eq_elt_dec e1 l1) as [_ | e1_not_in_l1]; [contradiction | idtac]. apply e1_not_in_l1; apply LP.in_permut_in with (l2' ++ l2''); trivial. apply LP.list_permut_sym; apply LP.list_permut_remove_hd with e1; trivial. Qed.
imports: List more_list list_permut Arith