proposition: Lemma text_sub_once : forall s c, text_sub s (c::s).
proof: Proof. Proof using. intros. apply~ tclosure_once. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat