∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.val)
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.val) {X : Cᵒᵖ}
  (r : ↑(R.val.obj X)) (m : ↑(A.val.obj X)) (Y : C) (f : Y ⟶ Opposite.unop X),
  let S := CategoryTheory.Presheaf.imageSieve α r ⊓ CategoryTheory.Presheaf.imageSieve φ m;
  ∀ (motive : S.arrows f → Prop) (h : S.arrows f),
    (∀ (r₀ : CategoryTheory.ToType (R₀.obj (Opposite.op Y)))
        (hr₀ :
          (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ =
            (CategoryTheory.ConcreteCategory.hom (R.val.map f.op)) r)
        (m₀ : CategoryTheory.ToType (M₀.presheaf.obj (Opposite.op Y)))
        (hm₀ :
          (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
            (CategoryTheory.ConcreteCategory.hom (A.val.map f.op)) m),
        motive ⋯) →
      motive h