{motive : Mathlib.Tactic.BicategoryLike.NormalizedHom → Sort u} →
  (ctorIdx : ℕ) →
    (t : Mathlib.Tactic.BicategoryLike.NormalizedHom) →
      ctorIdx = t.ctorIdx → Mathlib.Tactic.BicategoryLike.NormalizedHom.ctorElimType ctorIdx → motive t