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