fact: Fixpoint ac_size (t:term) : nat := match t with | Var v => 1 | Term f l => let ac_size_list := (fix ac_size_list (l : list term) {struct l} : nat := match l with | nil => 0 | t :: lt => ac_size t + ac_size_list lt end) in (match arity f with | AC => (length l) - 1 | C => 1 | Free _ => 1 end) + ac_size_list l end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)