{N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      {inst : Group N} →
        {inst_1 : Group E} →
          {inst_2 : Group G} →
            {S : GroupExtension N E G} →
              {P : Sort u} →
                {toFun : G → E} →
                  {rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom} →
                    {toFun' : G → E} →
                      {rightInverse_rightHom' : Function.RightInverse toFun' ⇑S.rightHom} →
                        { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
                            { toFun := toFun', rightInverse_rightHom := rightInverse_rightHom' } →
                          (toFun ≍ toFun' → P) → P