∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C}
  {p₁ : W ⟶ CategoryTheory.Limits.pullback (E.f i.1) (F.f i.2)}
  {p₂ : W ⟶ CategoryTheory.Limits.pullback (E.f j.1) (F.f j.2)} ⦃Y : C⦄ (f : Y ⟶ W)
  (motive : ((E.inter F).sieve₁ p₁ p₂).arrows f → Prop) (x : ((E.inter F).sieve₁ p₁ p₂).arrows f),
  (∀ (k : (E.inter F).I₁ i j) (a : Y ⟶ (E.inter F).Y k)
      (h₁ : CategoryTheory.CategoryStruct.comp f p₁ = CategoryTheory.CategoryStruct.comp a ((E.inter F).p₁ k))
      (h₂ : CategoryTheory.CategoryStruct.comp f p₂ = CategoryTheory.CategoryStruct.comp a ((E.inter F).p₂ k)),
      motive ⋯) →
    motive x