fact: Definition tmGetMyOption {X} (o : option_instance X) (err : string) : TemplateMonad X := match o with | my_Some x => ret x | my_None => tmFail err end.
imports: Ascii String Undecidability.L(Util.L_facts) MetaCoq(Template.All Template.Checker) Undecidability.Shared.Libs.PSL.Base MetaCoq.Utils.bytestring