{motive : Lean.Meta.FunIndParamKind → Sort u} →
  (t : Lean.Meta.FunIndParamKind) →
    motive Lean.Meta.FunIndParamKind.dropped →
      motive Lean.Meta.FunIndParamKind.param → motive Lean.Meta.FunIndParamKind.target → motive t