∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {W X Y Z : CategoryTheory.KleisliCat m} (f : W ⟶ X)
  (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)