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. unfold AUnary.Fun1. simpl. rewrite (Vcast_cons (is_unary_sig f)), Vcast_refl. simpl. rewrite max_0_r. intro h. rewrite (IH h). refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)