{motive : Lean.Meta.Grind.Arith.Cutsat.Search.Kind → Sort u} →
  (t : Lean.Meta.Grind.Arith.Cutsat.Search.Kind) →
    motive Lean.Meta.Grind.Arith.Cutsat.Search.Kind.rat → motive Lean.Meta.Grind.Arith.Cutsat.Search.Kind.int → motive t