fact: Definition m_listlist (A:Set) (xss : list (list A)) := match xss with nil => nil | (cons xs _) => (cons (length xss) (cons (length xs) nil)) end.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef