proposition: Lemma wf_on_rest : well_founded rpo_rest.
proof: Proof. unfold well_founded, rpo_rest; intro s; apply (Acc_inverse_image SN_term term rpo tt). destruct s; simpl; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term