∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : MonadAttach m] {P : β → m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) (hP : MonadAttach.CanReturn (P out) { down := false })
  (h_1 : (hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩)
  (h_2 : (hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩),
  (match ⟨{ down := false }, hP⟩ with
    | ⟨{ down := true }, hP⟩ => h_1 hP
    | ⟨{ down := false }, hP⟩ => h_2 hP) =
    h_2 hP