From MetaCoq.Template Require Export TemplateMonad.Core.
From Undecidability.L.Tactics Require Export Lsimpl mixedTactics ComputableTime Lbeta Computable ComputableTactics Lproc Lrewrite.
From Undecidability.L.Complexity Require Export UpToCNary.
Export Set Default Proof Using "Type".
From Undecidability.L.Tactics Require Export Lsimpl mixedTactics ComputableTime Lbeta Computable ComputableTactics Lproc Lrewrite.
From Undecidability.L.Complexity Require Export UpToCNary.
Export Set Default Proof Using "Type".