proposition: Lemma ac_one_step_at_top_top_eq : forall t1 t2, (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. unfold sym_refl; intros t1 t2 [Ac | [Ac | t1_eq_t2]]. inversion_clear Ac; simpl; trivial. inversion_clear Ac; simpl; trivial. subst t2; destruct t1; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)