proposition: Lemma rpo_rest_prec_eq : forall bb f g l, prec_eq Prec f g -> Acc (rpo_rest bb) (f, l) -> Acc (rpo_rest bb) (g, l).
proof: Proof. intros. destruct H0. apply Acc_intro. intros. apply H0. clear H0. destruct y. inversion H1. apply Top_gt_rest. apply prec_eq_prec1 with g. trivial. apply prec_eq_sym. trivial. trivial. trivial. apply Top_eq_lex_rest; trivial. assert (H13:= prec_eq_status Prec f g). assert (H14: status Prec f = status Prec g). apply H13. trivial. rewrite H14. trivial. apply prec_eq_transitive with g; trivial. apply prec_eq_sym; trivial. apply Top_eq_mul_rest; trivial. assert (H13:= prec_eq_status Prec f g). assert (H14: status Prec f = status Prec g). apply H13. trivial. rewrite H14. trivial. apply prec_eq_transitive with g; trivial. apply prec_eq_sym; trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)