proposition: Lemma wf_rpo : well_founded prec -> well_founded rpo.
proof: Proof. intro wf_prec; unfold well_founded; intro t; pattern t; apply term_rec3; clear t. intro v; apply Acc_intro; intros t lt_t_s; inversion lt_t_s. intros f l Acc_subterm; rewrite <- (projection_list_of_SN_terms l Acc_subterm). apply acc_build; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term