proposition: Lemma term_of_string_app : forall s1 s2, term_of_string (s1 ++ s2) = sub (sub_of_string s2) (term_of_string s1).
proof: Proof. induction s1. refl. intro. simpl. apply args_eq. rewrite IHs1. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)