proposition: Lemma ac_size_build_eq : forall f l, arity f = AC -> ac_size (build f l) = (length l - 1) + list_size ac_size l.
proof: Proof. intros f l Af; unfold build; simpl; destruct l as [ | t1 l]. rewrite quicksort_equation; simpl; rewrite Af; trivial. destruct l as [ | t2 l]. simpl; auto with arith. rewrite ac_size_unfold; rewrite Af; rewrite length_quicksort; apply (f_equal (fun n => length (t1 :: t2 :: l) -1 + n)); apply list_permut.permut_size with (@eq term). intros; subst; trivial. apply quick_permut_bis; auto. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching)