proposition: Lemma reset_reverse_term : forall t, reset (reverse_term t) = reverse_term t.
proof: Proof. intro t; pattern t; apply (term_ind_forall is_unary_sig); clear t; intros. refl. unfold reverse_term. rewrite !string_of_term_fun1, reset_term_of_string. refl. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)