{motive_1 : Lean.Server.Test.Runner.Client.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Server.Test.Runner.Client.StrictOrLazy
            (Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) Lean.Lsp.RpcRef →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed) → Sort u} →
          (t : Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) →
            ((t : Lean.Server.Test.Runner.Client.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed) →
                  Lean.Server.Test.Runner.Client.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      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.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) →
                      Lean.Server.Test.Runner.Client.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)) →
                        Lean.Server.Test.Runner.Client.MsgEmbed.below_4 t → motive_5 t) →
                      motive_4 t