{C : Type u} →
  {X : C} →
    {motive : Mathlib.Tactic.Coherence.LiftObj X → Sort u_1} →
      ((lift : CategoryTheory.FreeMonoidalCategory C) → motive { lift := lift }) →
        (t : Mathlib.Tactic.Coherence.LiftObj X) → motive t