{motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  (t : Lean.Widget.MsgEmbed) →
    ((a : Lean.Widget.CodeWithInfos) → motive_1 (Lean.Widget.MsgEmbed.expr a)) →
      ((a : Lean.Widget.InteractiveGoal) → motive_1 (Lean.Widget.MsgEmbed.goal a)) →
        ((wi : Lean.Widget.WidgetInstance) →
            (alt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → motive_1 (Lean.Widget.MsgEmbed.widget wi alt)) →
          ((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)) →
                      motive_1 (Lean.Widget.MsgEmbed.trace indent cls msg collapsed children)) →
            motive_1 t