∀ {C : Type u_2} {inst : CategoryTheory.Category.{u_1, u_2} C} {M N : CategoryTheory.Comonad C}
  (motive : CategoryTheory.ComonadHom M N → Prop) (h : CategoryTheory.ComonadHom M N),
  (∀ (app : (X : C) → M.obj X ⟶ N.obj X)
      (naturality :
        autoParam
          (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
            CategoryTheory.CategoryStruct.comp (M.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (N.map f))
          CategoryTheory.NatTrans.naturality._autoParam)
      (app_ε :
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (app X) (N.ε.app X) = M.ε.app X)
          CategoryTheory.ComonadHom.app_ε._autoParam)
      (app_δ :
        autoParam
          (∀ (X : C),
            CategoryTheory.CategoryStruct.comp (app X) (N.δ.app X) =
              CategoryTheory.CategoryStruct.comp (M.δ.app X)
                (CategoryTheory.CategoryStruct.comp (app (M.obj X)) (N.map (app X))))
          CategoryTheory.ComonadHom.app_δ._autoParam),
      motive { app := app, naturality := naturality, app_ε := app_ε, app_δ := app_δ }) →
    motive h