∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u')
  (X : I → C) (coversTop : J.CoversTop X) (generators : (i : I) → (M.over (X i)).GeneratingSections) (I_1 : Type u')
  (X_1 : I_1 → C) (coversTop_1 : J.CoversTop X_1) (generators_1 : (i : I_1) → (M.over (X_1 i)).GeneratingSections),
  ({ I := I, X := X, coversTop := coversTop, generators := generators } =
      { I := I_1, X := X_1, coversTop := coversTop_1, generators := generators_1 }) =
    (I = I_1 ∧ X ≍ X_1 ∧ generators ≍ generators_1)