fact: Definition rpo_mult_eval rpo_infos n l1 l2 := match remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2 with | None => mult_eval (rpo_eval rpo_infos n) l1 l2 | Some (nil, nil) => Some Equivalent | Some (nil, _ :: _) => Some Less_than | Some (_ :: _,nil) => Some Greater_than | Some (l, l') => mult_eval (rpo_eval rpo_infos n) l l' end.
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)