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