(motive : Lean.MVarId × Lean.Meta.SavedState → Sort u_1) →
  (__discr : Lean.MVarId × Lean.Meta.SavedState) →
    ((goal : Lean.MVarId) → (metaState : Lean.Meta.SavedState) → motive (goal, metaState)) → motive __discr