∀ {params : Lean.Lsp.CodeActionParams} {providerName : Lean.Name} {providerResultIndex : ℕ}
  {params_1 : Lean.Lsp.CodeActionParams} {providerName_1 : Lean.Name} {providerResultIndex_1 : ℕ},
  { params := params, providerName := providerName, providerResultIndex := providerResultIndex } =
      { params := params_1, providerName := providerName_1, providerResultIndex := providerResultIndex_1 } →
    params = params_1 ∧ providerName = providerName_1 ∧ providerResultIndex = providerResultIndex_1