{P : Sort u_1} →
  {R : Type u} →
    {L : Type v} →
      {M : Type w} →
        {N : Type w₁} →
          {inst : CommRing R} →
            {inst_1 : LieRing L} →
              {inst_2 : AddCommGroup M} →
                {inst_3 : AddCommGroup N} →
                  {inst_4 : Module R M} →
                    {inst_5 : Module R N} →
                      {inst_6 : LieRingModule L M} →
                        {inst_7 : LieRingModule L N} →
                          {t : M ≃ₗ⁅R,L⁆ N} →
                            {R' : Type u} →
                              {L' : Type v} →
                                {M' : Type w} →
                                  {N' : Type w₁} →
                                    {inst' : CommRing R'} →
                                      {inst'_1 : LieRing L'} →
                                        {inst'_2 : AddCommGroup M'} →
                                          {inst'_3 : AddCommGroup N'} →
                                            {inst'_4 : Module R' M'} →
                                              {inst'_5 : Module R' N'} →
                                                {inst'_6 : LieRingModule L' M'} →
                                                  {inst'_7 : LieRingModule L' N'} →
                                                    {t' : M' ≃ₗ⁅R',L'⁆ N'} →
                                                      R = R' →
                                                        L = L' →
                                                          M = M' →
                                                            N = N' →
                                                              inst ≍ inst' →
                                                                inst_1 ≍ inst'_1 →
                                                                  inst_2 ≍ inst'_2 →
                                                                    inst_3 ≍ inst'_3 →
                                                                      inst_4 ≍ inst'_4 →
                                                                        inst_5 ≍ inst'_5 →
                                                                          inst_6 ≍ inst'_6 →
                                                                            inst_7 ≍ inst'_7 →
                                                                              t ≍ t' →
                                                                                LieModuleEquiv.noConfusionType P t t'