∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {Z : a ⟶ a} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) t ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.counit t) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor t).inv h