proposition: Lemma reverse_term_reset : forall t, reverse_term (reset t) = reverse_term t.
proof: Proof. intro t; pattern t; apply (term_ind_forall is_unary_sig); clear t; intros. unfold reset, swap, single. simpl. rewrite (beq_refl beq_nat_ok). refl. rewrite reset_fun1. unfold reverse_term. rewrite !string_of_term_fun1, string_of_term_reset. refl. hyp. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)