{P : Sort u} →
  {N : Type u_1} →
    {E : Type u_2} →
      {G : Type u_3} →
        {inst : Group N} →
          {inst_1 : Group E} →
            {inst_2 : Group G} →
              {t : GroupExtension N E G} →
                {N' : Type u_1} →
                  {E' : Type u_2} →
                    {G' : Type u_3} →
                      {inst' : Group N'} →
                        {inst'_1 : Group E'} →
                          {inst'_2 : Group G'} →
                            {t' : GroupExtension N' E' G'} →
                              N = N' →
                                E = E' →
                                  G = G' →
                                    inst ≍ inst' →
                                      inst_1 ≍ inst'_1 →
                                        inst_2 ≍ inst'_2 → t ≍ t' → GroupExtension.noConfusionType P t t'