proposition: Lemma regexp_sub_wf : wf regexp_sub.
proof: Proof. Proof using. intros r. induction r; constructor; intros r' le; inverts~ le. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat