proposition: Lemma ac_size_eq : forall t1 t2, ac t1 t2 -> size t1 = size t2.
proof: Proof. intros t1 t2 H; refine (rwr_inv _ _ _ _ (@trans_eq nat) _ _ _ H). intros; apply ac_one_step_size_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)