{m : Type → Type} →
  {P : Sort u} →
    {toMonadExceptOf : MonadExceptOf Lean.Exception m} →
      {toMonadRef : Lean.MonadRef m} →
        {toAddErrorMessageContext : Lean.AddErrorMessageContext m} →
          {toMonadExceptOf' : MonadExceptOf Lean.Exception m} →
            {toMonadRef' : Lean.MonadRef m} →
              {toAddErrorMessageContext' : Lean.AddErrorMessageContext m} →
                { toMonadExceptOf := toMonadExceptOf, toMonadRef := toMonadRef,
                      toAddErrorMessageContext := toAddErrorMessageContext } =
                    { toMonadExceptOf := toMonadExceptOf', toMonadRef := toMonadRef',
                      toAddErrorMessageContext := toAddErrorMessageContext' } →
                  (toMonadExceptOf ≍ toMonadExceptOf' →
                      toMonadRef ≍ toMonadRef' → toAddErrorMessageContext ≍ toAddErrorMessageContext' → P) →
                    P