{motive_1 : Lean.Widget.HighlightedMsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) → Sort u} →
          ((a : Lean.Widget.HighlightedCodeWithInfos) → motive_1 (Lean.Widget.HighlightedMsgEmbed.expr a)) →
            ((a : Lean.Widget.InteractiveGoal) → motive_1 (Lean.Widget.HighlightedMsgEmbed.goal a)) →
              ((wi : Lean.Widget.WidgetInstance) →
                  (alt : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
                    motive_2 alt → motive_1 (Lean.Widget.HighlightedMsgEmbed.widget wi alt)) →
                ((indent : ℕ) →
                    (cls : Lean.Name) →
                      (msg : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
                        (collapsed : Bool) →
                          (children :
                              Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed))
                                (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                            motive_2 msg →
                              motive_3 children →
                                motive_1 (Lean.Widget.HighlightedMsgEmbed.trace indent cls msg collapsed children)) →
                  motive_1 Lean.Widget.HighlightedMsgEmbed.highlighted →
                    ((a : String) → motive_2 (Lean.Widget.TaggedText.text a)) →
                      ((a : Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                          motive_4 a → motive_2 (Lean.Widget.TaggedText.append a)) →
                        ((a : Lean.Widget.HighlightedMsgEmbed) →
                            (a_1 : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
                              motive_1 a → motive_2 a_1 → motive_2 (Lean.Widget.TaggedText.tag a a_1)) →
                          ((a : Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                              motive_4 a → motive_3 (Lean.Widget.StrictOrLazy.strict a)) →
                            ((a : Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
                                motive_3 (Lean.Widget.StrictOrLazy.lazy a)) →
                              ((toList : List (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                                  motive_5 toList → motive_4 { toList := toList }) →
                                motive_5 [] →
                                  ((head : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
                                      (tail : List (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                                        motive_2 head → motive_5 tail → motive_5 (head :: tail)) →
                                    (t :
                                        Lean.Widget.StrictOrLazy
                                          (Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed))
                                          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                                      motive_3 t