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