∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M] {f : G × G → M},
  groupCohomology.IsMulCoboundary₂ f →
    ∃ y, (ModuleCat.Hom.hom (groupCohomology.d₁₂ (Rep.ofMulDistribMulAction G M))) y = ⇑Additive.ofMul ∘ f