(motive : Batteries.CodeAction.TacticCodeActionEntry → Sort u_1) →
  (x : Batteries.CodeAction.TacticCodeActionEntry) →
    ((name : Lean.Name) → (kinds : Array Lean.Name) → motive { declName := name, tacticKinds := kinds }) → motive x