∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F), MonCat.Colimits.descFunLift F s MonCat.Colimits.Prequotient.one = 1