fact: Fixpoint list_size_mul (A : Type) (siz : A -> nat) (l : list A) {struct l} : list nat := match l with | nil => @nil nat | h :: tl => (siz h) :: (list_size_mul A siz tl) end.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)