proposition: Lemma term_of_string_epi : forall t, maxvar t = 0 -> term_of_string (string_of_term t) = t.
proof: Proof. intro t; pattern t; apply term_ind_forall; clear t. simpl in *. intros. subst. refl. intros f t IH. rewrite maxvar_fun1. intro. rewrite string_of_term_fun1. simpl. rewrite IH. refl. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)