proposition: Lemma text_sub_app : forall s s1 s2, s = s1 ++ s2 -> rclosure text_sub s2 s.
proof: Proof. Proof using. intros. rewrite rclosure_eq. subst. induction s1; rew_list. auto. inverts IHs1. left. applys~ (@trans_inv text) (s1++s2). rewrite <- H. left. apply text_sub_once. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat