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