{β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (Option β')} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩) →
                ((out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩) →
                  motive __do_lift