∀ {k G : Type u_1} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u_1, u_1} k G)
  (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains A).d 2 1))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).inv) ↑x) =
    0