{motive : Lean.Doc.CodeSuggestion → Sort u} →
  (t : Lean.Doc.CodeSuggestion) →
    ((role : Lean.Name) →
        (args moreInfo : Option String) → motive { role := role, args := args, moreInfo := moreInfo }) →
      motive t