∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {J : CategoryTheory.GrothendieckTopology C}
  {A : Type u_4} [inst_1 : CategoryTheory.Category.{u_2, u_4} A] (F : CategoryTheory.Sheaf J A) (X : C) (Y : A)
  (t : (F.val.comp (CategoryTheory.coyoneda.obj (Opposite.op Y))).obj (Opposite.op X)),
  ((fun t => CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a => ⋯.elim) t) t ∧
      ∀ (y : (F.val.comp (CategoryTheory.coyoneda.obj (Opposite.op Y))).obj (Opposite.op X)),
        (fun t => CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a => ⋯.elim) t) y → y = t) →
    ∀ (a : Y ⟶ F.val.obj (Opposite.op X)),
      (fun t => CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a => ⋯.elim) t) a