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