{P : Sort u} →
  {α : Type u_6} →
    {β : Type u_7} →
      {inst : Preorder α} →
        {inst_1 : Preorder β} →
          {inst_2 : Add α} →
            {inst_3 : Add β} →
              {t : α ≃+o β} →
                {α' : Type u_6} →
                  {β' : Type u_7} →
                    {inst' : Preorder α'} →
                      {inst'_1 : Preorder β'} →
                        {inst'_2 : Add α'} →
                          {inst'_3 : Add β'} →
                            {t' : α' ≃+o β'} →
                              α = α' →
                                β = β' →
                                  inst ≍ inst' →
                                    inst_1 ≍ inst'_1 →
                                      inst_2 ≍ inst'_2 →
                                        inst_3 ≍ inst'_3 → t ≍ t' → OrderAddMonoidIso.noConfusionType P t t'