∀ {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} {X Y : CategoryTheory.Sheaf J A}
  (motive : X.Hom Y → Prop) (h : X.Hom Y), (∀ (val : X.val ⟶ Y.val), motive { val := val }) → motive h