∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G G' : CategoryTheory.Subfunctor F),
  G ≤ G' →
    CategoryTheory.Presieve.IsSheaf J F →
      CategoryTheory.Presieve.IsSheaf J G'.toFunctor → CategoryTheory.Subfunctor.sheafify J G ≤ G'