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