proposition: Lemma ac_size_unfold : forall t, ac_size t = match t with | Var _ => 1 | Term f l => (match arity f with | AC => (length l) - 1 | C => 1 | Free _ => 1 end) + list_size ac_size l end.
proof: Proof. intro t; destruct t as [v | f l]; trivial; simpl. apply (f_equal (fun n => (match arity f with | AC => length l - 1 | C => 1 | Free _ => 1 end) + n)); induction l as [ | t l]; trivial. simpl; rewrite <- IHl; generalize (ac_size t); clear f t IHl; induction l as [ | t l]; simpl; trivial; intro n; rewrite (IHl (n + ac_size t)); rewrite (IHl (ac_size t)); auto with arith. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)