fact: Fixpoint maxl (A : Type) (l : list (nat * A)) : nat := match l with | nil => 0 | (n,_) :: l => Nat.max n (maxl _ l) end.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)