{P : Sort u} →
  {ref : Lean.Syntax} →
    {msg : Lean.MessageData} →
      {ref' : Lean.Syntax} →
        {msg' : Lean.MessageData} →
          Lean.Exception.error ref msg = Lean.Exception.error ref' msg' → (ref = ref' → msg = msg' → P) → P