proposition: Lemma list_size_mul_app: forall (A : Type) (siz : A -> nat) l1 l2, list_size_mul A siz (l1 ++ l2) = (list_size_mul A siz l1) ++ list_size_mul A siz l2.
proof: Proof. induction l1 as [ | a1 l1 ]; trivial. intros; simpl; rewrite IHl1; trivial. Qed.
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)