proposition: Lemma var_term_of_string : forall s, var (term_of_string s) = 0.
proof: Proof. induction s. refl. simpl term_of_string. rewrite var_fun1. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)