∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 a a_1 f