{motive : Lean.Parser.FirstTokens → Sort u} →
  (t : Lean.Parser.FirstTokens) →
    motive Lean.Parser.FirstTokens.epsilon →
      motive Lean.Parser.FirstTokens.unknown →
        ((a : List Lean.Parser.Token) → motive (Lean.Parser.FirstTokens.tokens a)) →
          ((a : List Lean.Parser.Token) → motive (Lean.Parser.FirstTokens.optTokens a)) → motive t