∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep k G} (x y : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) x =
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) y ↔
    ⇑x - ⇑y ∈ groupCohomology.coboundaries₂ A