fact: Parameter ac_cf_eq : forall t1 t2, ac t1 t2 -> canonical_form t1 = canonical_form t2.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)