{m : Type → Type} →
  {P : Sort u} →
    {tryCatchRuntimeEx tryCatchRuntimeEx' : {α : Type} → m α → (Lean.Exception → m α) → m α} →
      { tryCatchRuntimeEx := tryCatchRuntimeEx } = { tryCatchRuntimeEx := tryCatchRuntimeEx' } →
        (tryCatchRuntimeEx ≍ tryCatchRuntimeEx' → P) → P