proposition: Lemma reset_term_of_string : forall s, reset (term_of_string s) = term_of_string s.
proof: Proof. induction s. refl. unfold reset. simpl. apply args_eq. fold (reset (term_of_string s)). rewrite IHs. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)