∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y}
  (R : CategoryTheory.Sieve Z) (W : C) (h : W ⟶ X)
  (motive : (CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pushforward g R)).arrows h → Prop)
  (x : (CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pushforward g R)).arrows h),
  (∀ (y : W ⟶ Y) (hy : CategoryTheory.CategoryStruct.comp y f = h) (z : W ⟶ Z)
      (hR : CategoryTheory.CategoryStruct.comp z g = y) (hz : R.arrows z), motive ⋯) →
    motive x