{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Mon C} →
        {motive : M.Hom N → Sort u} →
          (t : M.Hom N) →
            ((hom : M.X ⟶ N.X) →
                [isMonHom_hom : CategoryTheory.IsMonHom hom] → motive { hom := hom, isMonHom_hom := isMonHom_hom }) →
              motive t