proposition: Lemma list_permut_map_acc : forall l l', list_permut (map tt l) (map tt l') -> Acc rpo_mul_rest_step l -> Acc rpo_mul_rest_step l'.
proof: Proof. intros l l' P A1; apply Acc_intro; intros l'' M2. inversion A1; apply H; inversion M2. subst l'0 l0; apply (List_mul_rest_step a ls lc); trivial. apply list_permut_trans with (map tt l'); trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term