{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {motive : CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X → Sort u_1} →
          (t : CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝¹ n X) →
            ({k k' : ℕ} →
                (hk : k < n) →
                  (hk' : k' < n) →
                    (a : (X k hk).fst) →
                      (a_1 : (X k' hk').fst) →
                        motive (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk hk' a a_1)) →
              ({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') →
                            motive
                              (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk hk' j j' a a_1)) →
                motive t