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