∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  [inst_1 : SizeOf C] {k k' : ℕ} (hk : k < n) (hk' : k' < n) (j : (X k hk).fst) (j' : (X k' hk').fst)
  (a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j'),
  sizeOf (CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk hk' j j' a a_1) =
    1 + sizeOf k + sizeOf k' + sizeOf hk + sizeOf hk' + sizeOf j + sizeOf j' + sizeOf a + sizeOf a_1