{motive : Lean.ErrorExplanation → Sort u} →
  (t : Lean.ErrorExplanation) →
    ((doc : String) →
        (metadata : Lean.ErrorExplanation.Metadata) →
          (declLoc? : Option Lean.DeclarationLocation) →
            motive { doc := doc, metadata := metadata, declLoc? := declLoc? }) →
      motive t