{motive : Lean.Meta.Grind.CheckResult → Sort u} →
  (t : Lean.Meta.Grind.CheckResult) →
    motive Lean.Meta.Grind.CheckResult.none →
      motive Lean.Meta.Grind.CheckResult.progress →
        motive Lean.Meta.Grind.CheckResult.propagated → motive Lean.Meta.Grind.CheckResult.closed → motive t