proposition: Theorem ac_cf_eq : forall t1 t2, ac t1 t2 -> canonical_form t1 = canonical_form t2.
proof: Proof. unfold ac, th_eq; intros t1 t2 H. refine (rwr_inv _ _ _ _ (@trans_eq term) _ _ _ H). clear t1 t2 H; intros t1 t2 H; apply ac_one_step_cf_eq; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)