{i : Type u} →
  {b : Type v} →
    {p : Type w} →
      {motive_1 : Lean.Doc.Part i b p → Sort u_1} →
        {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} →
          {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1} →
            ((title : Array (Lean.Doc.Inline i)) →
                (titleString : String) →
                  (metadata : Option p) →
                    (content : Array (Lean.Doc.Block i b)) →
                      (subParts : Array (Lean.Doc.Part i b p)) →
                        motive_2 subParts →
                          motive_1
                            { title := title, titleString := titleString, metadata := metadata, content := content,
                              subParts := subParts }) →
              ((toList : List (Lean.Doc.Part i b p)) → motive_3 toList → motive_2 { toList := toList }) →
                motive_3 [] →
                  ((head : Lean.Doc.Part i b p) →
                      (tail : List (Lean.Doc.Part i b p)) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                    (t : List (Lean.Doc.Part i b p)) → motive_3 t