∀ {C : Type u_2} {inst : CategoryTheory.Category.{u_1, u_2} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} (motive : I₁.Relation I₂ → Prop) (h : I₁.Relation I₂),
  (∀ (Z : C) (g₁ : Z ⟶ I₁.Y) (g₂ : Z ⟶ I₂.Y)
      (w :
        autoParam (CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f)
          CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam),
      motive { Z := Z, g₁ := g₁, g₂ := g₂, w := w }) →
    motive h