∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()