fact: Fixpoint canonical_form (t : term) : term := match t with | Var _ => t | Term f l => Term f (match arity f with | Free _ => map canonical_form l | C => quicksort (map canonical_form l) | AC => quicksort (flatten f (map canonical_form l)) end) end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)