∀ {C : Type u_2} {inst : CategoryTheory.Category.{u_1, u_2} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (motive : S.Relation → Prop) (h : S.Relation),
  (∀ (fst snd : S.Arrow) (r : fst.Relation snd), motive { fst := fst, snd := snd, r := r }) → motive h