(motive : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") → Sort u_1) →
  (attrs? : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) →
    ((attrs? : Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") → motive (some attrs?)) →
      ((x : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) → motive x) → motive attrs?