{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {F : CategoryTheory.Functor C C} →
      {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} →
        {P : Sort u_1} →
          {f : V₀.V ⟶ V₁.V} →
            {h :
                autoParam
                  (CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str)
                  CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam} →
              {f' : V₀.V ⟶ V₁.V} →
                {h' :
                    autoParam
                      (CategoryTheory.CategoryStruct.comp V₀.str (F.map f') =
                        CategoryTheory.CategoryStruct.comp f' V₁.str)
                      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam} →
                  { f := f, h := h } = { f := f', h := h' } → (f ≍ f' → P) → P