{motive : Lean.Exception → Sort u} →
  (t : Lean.Exception) →
    ((ref : Lean.Syntax) → (msg : Lean.MessageData) → motive (Lean.Exception.error ref msg)) →
      ((id : Lean.InternalExceptionId) → (extra : Lean.KVMap) → motive (Lean.Exception.internal id extra)) → motive t