proposition: Lemma trans_text_sub : trans text_sub.
proof: Proof. Proof using. apply trans_tclosure. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat