{motive_1 : Lean.Server.Test.Runner.Client.HighlightedMsgEmbed → Sort u} →
  (t : Lean.Server.Test.Runner.Client.HighlightedMsgEmbed) →
    ((a : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.HighlightedSubexprInfo) →
        motive_1 (Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.expr a)) →
      ((a : Lean.Server.Test.Runner.Client.InteractiveGoal) →
          motive_1 (Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.goal a)) →
        ((wi : Lean.Server.Test.Runner.Client.WidgetInstance) →
            (alt : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.HighlightedMsgEmbed) →
              motive_1 (Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.widget wi alt)) →
          ((indent : ℕ) →
              (cls : Lean.Name) →
                (msg : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.HighlightedMsgEmbed) →
                  (collapsed : Bool) →
                    (children :
                        Lean.Server.Test.Runner.Client.StrictOrLazy
                          (Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.HighlightedMsgEmbed))
                          Lean.Lsp.RpcRef) →
                      motive_1
                        (Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.trace indent cls msg collapsed children)) →
            motive_1 Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.highlighted → motive_1 t