{motive : Lean.MetavarContext.UnivMVarParamResult → Sort u} →
  ((mctx : Lean.MetavarContext) →
      (newParamNames : Array Lean.Name) →
        (nextParamIdx : ℕ) →
          (expr : Lean.Expr) →
            motive { mctx := mctx, newParamNames := newParamNames, nextParamIdx := nextParamIdx, expr := expr }) →
    (t : Lean.MetavarContext.UnivMVarParamResult) → motive t