{α : Type u_1} →
  (motive : Lean.Widget.TaggedText α → Sort u_2) →
    (x : Lean.Widget.TaggedText α) →
      ((s : String) → motive (Lean.Widget.TaggedText.text s)) →
        ((as : Array (Lean.Widget.TaggedText α)) → motive (Lean.Widget.TaggedText.append as)) →
          ((a : Lean.Widget.TaggedText α) → motive a) → motive x