proposition: Lemma string_of_term_epi : forall s, string_of_term (term_of_string s) = s.
proof: Proof. induction s; intros. refl. simpl term_of_string. rewrite string_of_term_fun1, IHs. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)