proposition: Lemma equiv_acc_rpo : forall bb t t', equiv t t' -> Acc (rpo bb) t -> Acc (rpo bb) t'.
proof: Proof. intros bb t t' t_eq_t' Acc_t; apply Acc_intro. intro s; rewrite <- (equiv_rpo_equiv_1 _ t_eq_t'). inversion Acc_t as [H]; apply (H s); 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)