{motive : Lean.Parser.ParserContextCore → Sort u} →
  (t : Lean.Parser.ParserContextCore) →
    ((toInputContext : Lean.Parser.InputContext) →
        (toParserModuleContext : Lean.Parser.ParserModuleContext) →
          (toCacheableParserContext : Lean.Parser.CacheableParserContext) →
            (tokens : Lean.Parser.TokenTable) →
              motive
                { toInputContext := toInputContext, toParserModuleContext := toParserModuleContext,
                  toCacheableParserContext := toCacheableParserContext, tokens := tokens }) →
      motive t