{J : Type u_1} →
  (motive : CategoryTheory.WithTerminal J → Sort u_2) →
    (x : CategoryTheory.WithTerminal J) →
      ((a : J) → motive (CategoryTheory.WithTerminal.of a)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x