{P : Sort u} →
  {stx : Lean.TSyntax `tactic} →
    {msg : Lean.MessageData} →
      {stx' : Lean.TSyntax `tactic} →
        {msg' : Lean.MessageData} →
          Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx msg =
              Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝¹ stx' msg' →
            (stx = stx' → msg = msg' → P) → P