{A B : GrpCat} →
  {f : A ⟶ B} →
    {P : Sort u_1} →
      {a a' : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)} →
        GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a = GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a' →
          (a ≍ a' → P) → P