fact: Definition rpo_term : relation (symbol * list SN_term) := fun f_l g_l' => match f_l with | (f,l) => match g_l' with | (g,l') => if F.eq_symbol_dec f g then match status f with | Lex => rpo_lex_rest l l' | Mul => rpo_mul_rest l l' end else prec f g end end.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term