proposition: Lemma ac_top_eq : forall t1 t2 : term, ac 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; induction Ac. inversion H as [ H1 H2 H' H4 H5 | f l1 l2 H' H1 H2]; subst; trivial. apply ac_one_step_top_eq; assumption. generalize (ac_one_step_top_eq H). destruct x as [ v1 | f1 l1 ]; destruct y as [ v2 | f2 l2 ]; destruct z as [ v3 | f3 l3 ]; trivial. intro; apply trans_eq with v2; assumption. contradiction. contradiction. intro; apply trans_eq with f2; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)