{motive : Mathlib.Tactic.BicategoryLike.Mor₂ → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.Mor₂) →
    ((t : Mathlib.Tactic.BicategoryLike.Mor₂) → Mathlib.Tactic.BicategoryLike.Mor₂.below t → motive t) → motive t