{P : Sort u} →
  {doc : Lean.Server.DocumentMeta} →
    {kind : Lean.Server.GoToKind} →
      {infoTree? : Option Lean.Elab.InfoTree} →
        {originInfo? : Option Lean.Elab.Info} →
          {children : Lean.PersistentArray Lean.Elab.InfoTree} →
            {doc' : Lean.Server.DocumentMeta} →
              {kind' : Lean.Server.GoToKind} →
                {infoTree?' : Option Lean.Elab.InfoTree} →
                  {originInfo?' : Option Lean.Elab.Info} →
                    {children' : Lean.PersistentArray Lean.Elab.InfoTree} →
                      { doc := doc, kind := kind, infoTree? := infoTree?, originInfo? := originInfo?,
                            children := children } =
                          { doc := doc', kind := kind', infoTree? := infoTree?', originInfo? := originInfo?',
                            children := children' } →
                        (doc = doc' →
                            kind = kind' →
                              infoTree? = infoTree?' → originInfo? = originInfo?' → children = children' → P) →
                          P