proposition: Lemma wf_rpo_term : well_founded prec -> well_founded rpo_term.
proof: Proof. intro wf_prec; unfold well_founded in *; destruct a; rename s into f; generalize l; clear l; pattern f; refine (well_founded_ind wf_prec _ _ f); clear f; intros f IHf l; pattern l; assert (forall g, f=g -> status g = status f). intros; subst f; trivial. destruct (status f); generalize (H f (refl_equal _)); clear H; intro H. pattern l; refine (well_founded_ind wf_on_lex_rest _ _ l); clear l; intros l IHl; apply Acc_intro; intros y; destruct y; simpl; elim (F.eq_symbol_dec s f); intro eq1. subst s; rewrite H; intros; apply IHl; trivial. intros; apply IHf; trivial. pattern l; refine (well_founded_ind wf_on_mul_rest _ _ l); clear l; intros l IHl; apply Acc_intro; intros y; destruct y; simpl; elim (F.eq_symbol_dec s f); intro eq1. subst s; rewrite H; intros; apply IHl; trivial. intros; apply IHf; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term