proposition: Lemma wf_rpo : well_founded (prec Prec) -> forall bb, well_founded (rpo bb).
proof: Proof. intros wf_prec bb; unfold well_founded; intro t; pattern t; apply term_rec3_mem; clear t. intro v; apply Acc_intro; intros s s_lt_t; inversion s_lt_t. intros f l Acc_l; apply (acc_build wf_prec bb (f,l)); 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)