{motive : Lean.Meta.Closure.MkValueTypeClosureResult → Sort u} →
  ((levelParams : Array Lean.Name) →
      (type value : Lean.Expr) →
        (levelArgs : Array Lean.Level) →
          (exprArgs : Array Lean.Expr) →
            motive
              { levelParams := levelParams, type := type, value := value, levelArgs := levelArgs,
                exprArgs := exprArgs }) →
    (t : Lean.Meta.Closure.MkValueTypeClosureResult) → motive t