{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.FinitaryExtensive C → Sort u_1} →
      (t : CategoryTheory.FinitaryExtensive C) →
        ([hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C] →
            [hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C] →
              (van_kampen' :
                  ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c),
                    CategoryTheory.IsVanKampenColimit c) →
                motive ⋯) →
          motive t