∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePushoutShape J → Sort u_2) (j : J) (h_1 : Unit → motive none)
  (h_2 : (j : J) → motive (some j)),
  (match some j with
    | none => h_1 ()
    | some j => h_2 j) =
    h_2 j