∀ {indent : ℕ} {cls : Lean.Name} {msg : Lean.Widget.TaggedText Lean.Widget.MsgEmbed} {collapsed : Bool}
  {children :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)}
  {indent_1 : ℕ} {cls_1 : Lean.Name} {msg_1 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed} {collapsed_1 : Bool}
  {children_1 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)},
  Lean.Widget.MsgEmbed.trace indent cls msg collapsed children =
      Lean.Widget.MsgEmbed.trace indent_1 cls_1 msg_1 collapsed_1 children_1 →
    indent = indent_1 ∧ cls = cls_1 ∧ msg = msg_1 ∧ collapsed = collapsed_1 ∧ children = children_1