{motive : Lean.Meta.ParamInfo → Sort u} →
  ((binderInfo : Lean.BinderInfo) →
      (hasFwdDeps : Bool) →
        (backDeps : Array ℕ) →
          (isProp isDecInst isInstance higherOrderOutParam dependsOnHigherOrderOutParam : Bool) →
            motive
              { binderInfo := binderInfo, hasFwdDeps := hasFwdDeps, backDeps := backDeps, isProp := isProp,
                isDecInst := isDecInst, isInstance := isInstance, higherOrderOutParam := higherOrderOutParam,
                dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam }) →
    (t : Lean.Meta.ParamInfo) → motive t