∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) (ι : Type (max u_2 u_1)) (Y : ι → C) (f : (i : ι) → Y i ⟶ S)
  (j : (Z : C) → (g : Z ⟶ S) → CategoryTheory.Presieve.ofArrows Y f g → E.I₀)
  (motive : (Z : C) → (g : Z ⟶ S) → g ∈ (E.restrictIndex fun i => j (Y i) (f i) ⋯).presieve₀ → Prop) (Z : C) (g : Z ⟶ S)
  (x : g ∈ (E.restrictIndex fun i => j (Y i) (f i) ⋯).presieve₀),
  (∀ (i : (E.restrictIndex fun i => j (Y i) (f i) ⋯).I₀),
      motive ((E.restrictIndex fun i => j (Y i) (f i) ⋯).X i) ((E.restrictIndex fun i => j (Y i) (f i) ⋯).f i) ⋯) →
    motive Z g x