(motive : Lean.Meta.ReduceMatcherResult → Sort u_1) →
  (__discr : Lean.Meta.ReduceMatcherResult) →
    ((value : Lean.Expr) → motive (Lean.Meta.ReduceMatcherResult.reduced value)) →
      ((x : Lean.Meta.ReduceMatcherResult) → motive x) → motive __discr