{α : Type} →
  (motive : α × Lean.Elab.Tactic.SavedState → Sort u_1) →
    (x : α × Lean.Elab.Tactic.SavedState) →
      ((val : α) → (state : Lean.Elab.Tactic.SavedState) → motive (val, state)) → motive x