{P : Sort u} →
  {indent : ℕ} →
    {cls : Lean.Name} →
      {msg : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed} →
        {collapsed : Bool} →
          {children :
              Lean.Server.Test.Runner.Client.StrictOrLazy
                (Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) Lean.Lsp.RpcRef} →
            {indent' : ℕ} →
              {cls' : Lean.Name} →
                {msg' : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed} →
                  {collapsed' : Bool} →
                    {children' :
                        Lean.Server.Test.Runner.Client.StrictOrLazy
                          (Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) Lean.Lsp.RpcRef} →
                      Lean.Server.Test.Runner.Client.MsgEmbed.trace indent cls msg collapsed children =
                          Lean.Server.Test.Runner.Client.MsgEmbed.trace indent' cls' msg' collapsed' children' →
                        (indent = indent' →
                            cls = cls' → msg = msg' → collapsed = collapsed' → children = children' → P) →
                          P