proposition: Lemma list_permut_map_acc : forall bb l l', permut0 equiv l l' -> Acc (rpo_mul_step_rest bb) l -> Acc (rpo_mul_step_rest bb) l'.
proof: Proof. intros bb l l' P A1; apply Acc_intro; intros l'' M2. inversion A1 as [H]; apply H; inversion M2 as [k' k'' Acc_l' Acc_l'' H']; subst. inversion H' as [a ls lc k' k'' P'' P' ls_lt_a]; subst. apply Rpo_mul_step_rest; trivial. intros s s_in_l; apply Acc_l'; rewrite <- (mem_permut0_mem equiv_equiv s P); trivial. apply (@List_mul_step bb a ls lc); trivial; apply permut0_trans with l'; trivial. apply equiv_equiv. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)