proposition: Lemma no_need_of_instance : forall t1 t2, axiom (sym_refl unit_one_step_at_top) t1 t2 -> (sym_refl unit_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'; simpl. left; apply left_unit; trivial. left; apply right_unit; trivial. right; left; apply left_unit; trivial. right; left; apply right_unit; trivial. right; right; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)