{P : Sort u_3} →
  {R : Type u} →
    {inst : Ring R} →
      {Q : Type v} →
        {inst_1 : AddCommGroup Q} →
          {inst_2 : Module R Q} →
            {M : Type u_1} →
              {N : Type u_2} →
                {inst_3 : AddCommGroup M} →
                  {inst_4 : AddCommGroup N} →
                    {inst_5 : Module R M} →
                      {inst_6 : Module R N} →
                        {i : M →ₗ[R] N} →
                          {f : M →ₗ[R] Q} →
                            {t : Module.Baer.ExtensionOf i f} →
                              {R' : Type u} →
                                {inst' : Ring R'} →
                                  {Q' : Type v} →
                                    {inst'_1 : AddCommGroup Q'} →
                                      {inst'_2 : Module R' Q'} →
                                        {M' : Type u_1} →
                                          {N' : Type u_2} →
                                            {inst'_3 : AddCommGroup M'} →
                                              {inst'_4 : AddCommGroup N'} →
                                                {inst'_5 : Module R' M'} →
                                                  {inst'_6 : Module R' N'} →
                                                    {i' : M' →ₗ[R'] N'} →
                                                      {f' : M' →ₗ[R'] Q'} →
                                                        {t' : Module.Baer.ExtensionOf i' f'} →
                                                          R = R' →
                                                            inst ≍ inst' →
                                                              Q = Q' →
                                                                inst_1 ≍ inst'_1 →
                                                                  inst_2 ≍ inst'_2 →
                                                                    M = M' →
                                                                      N = N' →
                                                                        inst_3 ≍ inst'_3 →
                                                                          inst_4 ≍ inst'_4 →
                                                                            inst_5 ≍ inst'_5 →
                                                                              inst_6 ≍ inst'_6 →
                                                                                i ≍ i' →
                                                                                  f ≍ f' →
                                                                                    t ≍ t' →
                                                                                      Module.Baer.ExtensionOf.noConfusionType
                                                                                        P t t'