proposition: Lemma ac_one_step_top_eq : forall t1 t2 : term, one_step (sym_refl ac_one_step_at_top) t1 t2 -> match t1, t2 with | Var x1, Var x2 => x1 = x2 | Term _ _, Var _ => False | Var _, Term _ _ => False | Term f1 _, Term f2 _ => f1 = f2 end.
proof: Proof. intros t1 t2 Ac; inversion Ac; trivial. apply ac_one_step_at_top_top_eq; apply no_need_of_instance; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)