fact: Record rpo_inf : Type := { bb : nat; rpo_l : list (term*term); rpo_eq_l : list (term*term); equiv_l : list (term*term); rpo_l_valid : forall t t', In (t,t') rpo_l -> rpo bb t t'; rpo_eq_valid : forall t t', In (t,t') rpo_eq_l -> rpo_eq bb t t'; equiv_l_valid : forall t t', In (t,t') equiv_l -> equiv t t' }.
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)