{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) →
            (__do_lift : Subtype (MonadAttach.CanReturn (P out))) →
              ((hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩) →
                ((hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩) →
                  motive __do_lift