{P : Sort u} →
  {id : Lean.InternalExceptionId} →
    {extra : optParam Lean.KVMap { }} →
      {id' : Lean.InternalExceptionId} →
        {extra' : optParam Lean.KVMap { }} →
          Lean.Exception.internal id extra = Lean.Exception.internal id' extra' → (id = id' → extra = extra' → P) → P