(motive : Lean.Meta.AbstractMVarsResult → Sort u_1) →
  (__discr : Lean.Meta.AbstractMVarsResult) →
    ((levelParams : Array Lean.Name) →
        (mvars : Array Lean.Expr) →
          (proof : Lean.Expr) → motive { paramNames := levelParams, mvars := mvars, expr := proof }) →
      motive __discr