proposition: Lemma term_of_string_epi : forall t, maxvar t = 0 -> ATerm_of_String.term_of_string (string_of_term t) = Ft HF t.
proof: Proof. intro t; pattern t; apply (term_ind_forall is_unary_sig); clear t; intros. simpl. simpl in H. subst. refl. rewrite string_of_term_fun1. unfold ATerm_of_String.term_of_string; fold (ATerm_of_String.term_of_string (string_of_term t)). rewrite H. unfold Fun1. unfold Ft at -1. rewrite Vmap_cast, Vcast_cast. simpl Vmap. apply args_eq. rewrite Vcast_refl. refl. rewrite maxvar_fun1 in H0. hyp. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)