{motive : Lean.Parser.ParserExtension.OLeanEntry → Sort u} →
  (t : Lean.Parser.ParserExtension.OLeanEntry) →
    t.ctorIdx = 0 → ((val : Lean.Parser.Token) → motive (Lean.Parser.ParserExtension.OLeanEntry.token val)) → motive t