{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Comonad C} →
      {motive : CategoryTheory.ComonadHom M N → Sort u} →
        (t : CategoryTheory.ComonadHom M N) →
          ((toNatTrans : CategoryTheory.NatTrans M.toFunctor N.toFunctor) →
              (app_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X) →
                (app_δ :
                    ∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
                        CategoryTheory.CategoryStruct.comp (M.δ.app X)
                          (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X)))) →
                  motive { toNatTrans := toNatTrans, app_ε := app_ε, app_δ := app_δ }) →
            motive t