{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} →
          (t : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
            ((t : Lean.Widget.HighlightedMsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed) →
                  Lean.Widget.HighlightedMsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.HighlightedMsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                      Lean.Widget.HighlightedMsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed)) →
                        Lean.Widget.HighlightedMsgEmbed.below_4 t → motive_5 t) →
                      motive_2 t ×' Lean.Widget.HighlightedMsgEmbed.below_1 t