{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} →
          {Z : C} →
            {h : Z ⟶ X} →
              [SizeOf C] →
                [⦃Y : C⦄ → (a : Y ⟶ X) → SizeOf (S a)] →
                  [⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (a : S f) → ⦃Y_1 : C⦄ → (a_1 : Y_1 ⟶ Y) → SizeOf (R a a_1)] →
                    S.BindStruct R h → ℕ