proposition: Lemma acc_lex_drop_proof : forall s t l, tt s = tt t -> Acc rpo_lex_rest (s::l) -> Acc rpo_lex_rest (t::l).
proof: Proof. intros s t l s_eq_t Acc_s. apply Acc_intro; intros l' lt_l'_l; apply Acc_inv with (s :: l); trivial; inversion lt_l'_l. subst l' t0 l'0; apply List_gt_rest; trivial; unfold rpo_rest in *; rewrite s_eq_t; trivial. subst l' t0 l'0; apply List_eq_rest; trivial; rewrite s_eq_t; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term