{motive : Lean.Parser.ParserContextCore → Sort u} →
  ((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 }) →
    (t : Lean.Parser.ParserContextCore) → motive t