proposition: Lemma no_need_of_instance : forall t1 t2, axiom (sym_refl ac_one_step_at_top) t1 t2 -> (sym_refl ac_one_step_at_top) t1 t2.
proof: Proof. unfold sym_refl; intros t1 t2 H. inversion_clear H as [ u1 u2 sigma H']; destruct H' as [H' | [H' | H']]. inversion_clear H'. left; simpl; apply a_axiom; trivial. left; simpl; apply c_axiom; trivial. inversion_clear H'. right; left; simpl; apply a_axiom; trivial. right; left; simpl; apply c_axiom; trivial. right; right; 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)