proposition: Lemma text_sub_wf : wf text_sub.
proof: Proof. Proof using. lets: wf_tclosure. unfold text_sub. solve_wf. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat