proposition: Lemma ac_one_step_size_eq : forall t1 t2, one_step (sym_refl ac_one_step_at_top) t1 t2 -> size t1 = size t2.
proof: Proof. intros t1; pattern t1; apply term_rec3; clear t1. intros v1 t2 H; inversion_clear H as [H1 H2 H' | f l1 l2 H']. apply sym_refl_ac_one_step_at_top_size_eq; apply no_need_of_instance; trivial. intros f l1 IHl1 t2 H; inversion_clear H as [ H1 H2 Hroot | H1 H2 l2 Hsub]. apply sym_refl_ac_one_step_at_top_size_eq; apply no_need_of_instance; trivial. assert (H : list_size size l1 = list_size size l2). generalize l2 Hsub; clear l2 Hsub; induction l1 as [ | t1 l1]; intros l2 Hsub; inversion_clear Hsub. simpl; apply (f_equal (fun n => n + list_size size l1)); apply IHl1; trivial; left; trivial. simpl; apply (f_equal (fun n => size t1 + n)); apply IHl0; trivial; intros; apply IHl1; trivial; right; trivial. do 2 rewrite size_unfold; rewrite H; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)