{P : Sort u} →
  {ident : Lean.Lsp.RefIdent} →
    {aliases : Array Lean.Lsp.RefIdent} →
      {range : Lean.Lsp.Range} →
        {stx : Lean.Syntax} →
          {ci : Lean.Elab.ContextInfo} →
            {info : Lean.Elab.Info} →
              {isBinder : Bool} →
                {ident' : Lean.Lsp.RefIdent} →
                  {aliases' : Array Lean.Lsp.RefIdent} →
                    {range' : Lean.Lsp.Range} →
                      {stx' : Lean.Syntax} →
                        {ci' : Lean.Elab.ContextInfo} →
                          {info' : Lean.Elab.Info} →
                            {isBinder' : Bool} →
                              { ident := ident, aliases := aliases, range := range, stx := stx, ci := ci, info := info,
                                    isBinder := isBinder } =
                                  { ident := ident', aliases := aliases', range := range', stx := stx', ci := ci',
                                    info := info', isBinder := isBinder' } →
                                (ident = ident' →
                                    aliases = aliases' →
                                      range = range' →
                                        stx = stx' → ci = ci' → info = info' → isBinder = isBinder' → P) →
                                  P