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