{motive : Lean.Meta.ProjReductionKind → Sort u} →
  (t : Lean.Meta.ProjReductionKind) →
    motive Lean.Meta.ProjReductionKind.no →
      motive Lean.Meta.ProjReductionKind.yes →
        motive Lean.Meta.ProjReductionKind.yesWithDelta → motive Lean.Meta.ProjReductionKind.yesWithDeltaI → motive t