proposition: Lemma wf_on_lex_rest : well_founded rpo_lex_rest.
proof: Proof. unfold well_founded; intro a; pattern a; apply list_rec2; clear a; induction n; intros l L; destruct l. apply Acc_intro; intros l' lt_l'_l; inversion lt_l'_l. simpl in L; absurd (S(length l) <= 0); auto with arith. apply Acc_intro; intros l' lt_l'_l; inversion lt_l'_l. simpl in L; generalize (le_S_n _ _ L); clear L; intro L. generalize l L; clear l L; pattern s; apply (well_founded_induction_type wf_on_rest); clear s; intros s IH l L. generalize (IHn l L); intro Acc_l; induction Acc_l; rename x into l. apply Acc_intro; intros l' lt_l'_l; inversion lt_l'_l. subst l' t l'0; apply IH; trivial; rewrite H5; trivial. subst l' t l'0; apply acc_lex_drop_proof with s. apply sym_eq; trivial. apply H0; trivial; rewrite (rpo_lex_rest_same_length _ _ H5); trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term