(motive : Lean.Meta.FunIndParamKind → Sort u_1) →
  (kind : Lean.Meta.FunIndParamKind) →
    (Unit → motive Lean.Meta.FunIndParamKind.target) → ((x : Lean.Meta.FunIndParamKind) → motive x) → motive kind