{m : Type u → Type v} →
  [inst : Functor m] →
    [inst_1 : LawfulFunctor m] →
      {motive : MonadSatisfying m → Sort u_1} →
        (t : MonadSatisfying m) →
          ((satisfying : {α : Type u} → {p : α → Prop} → {x : m α} → SatisfiesM p x → m { a // p a }) →
              (val_eq :
                  ∀ {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x), Subtype.val <$> satisfying h = x) →
                motive { satisfying := satisfying, val_eq := val_eq }) →
            motive t