∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  (J : CategoryTheory.GrothendieckTopology C) [self : F.IsPrestack J] {S : C} (M N : ↑(F.obj { as := Opposite.op S })),
  CategoryTheory.Presheaf.IsSheaf (J.over S) (F.presheafHom M N)