{m : Type u → Type v} →
  {motive : MonadAttach m → Sort u_1} →
    ((CanReturn : {α : Type u} → m α → α → Prop) →
        (attach : {α : Type u} → (x : m α) → m (Subtype (CanReturn x))) →
          motive { CanReturn := CanReturn, attach := attach }) →
      (t : MonadAttach m) → motive t