fact: Definition build (f : symbol) l := match l with | t :: nil => t | _ => Term f (quicksort l) end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)