From MetaCoq.Template Require Export TemplateMonad.Core.
From Undecidability.L.Tactics Require Export Lsimpl Lbeta Computable ComputableTactics Lproc Lrewrite.
From Undecidability.L.Tactics Require Export Lsimpl Lbeta Computable ComputableTactics Lproc Lrewrite.