∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat}
  {inst_3 : J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)} {M : SheafOfModules R}
  {generators : M.GeneratingSections} {relations : (CategoryTheory.Limits.kernel generators.π).GeneratingSections}
  {generators_1 : M.GeneratingSections}
  {relations_1 : (CategoryTheory.Limits.kernel generators_1.π).GeneratingSections},
  { generators := generators, relations := relations } = { generators := generators_1, relations := relations_1 } →
    generators = generators_1 ∧ relations ≍ relations_1