{motive : Lean.Meta.Grind.SavedState → Sort u} →
  (t : Lean.Meta.Grind.SavedState) →
    ((«meta» : Lean.Meta.SavedState) → (grind : Lean.Meta.Grind.State) → motive { «meta» := «meta», grind := grind }) →
      motive t