proposition: Lemma sym_refl_ac_one_step_at_top_size_eq : forall t1 t2, (sym_refl ac_one_step_at_top) t1 t2 -> size t1 = size t2.
proof: Proof. intros t1 t2; unfold sym_refl; intros [H | [H | H]]. apply ac_one_step_at_top_size_eq; trivial. apply sym_eq; apply ac_one_step_at_top_size_eq; trivial. subst; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)