∀ {J : Type u_1} (x : CategoryTheory.Limits.WidePullbackShape J),
  (match
      match x with
      | some x => CategoryTheory.WithTerminal.of { as := x }
      | none => CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of x => some x.as
    | CategoryTheory.WithTerminal.star => none) =
    x