{i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      ((contents : Array (Lean.Doc.Inline i)) → motive_1 (Lean.Doc.Block.para contents)) →
                        ((content : String) → motive_1 (Lean.Doc.Block.code content)) →
                          ((items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              motive_2 items → motive_1 (Lean.Doc.Block.ul items)) →
                            ((start : ℤ) →
                                (items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                  motive_2 items → motive_1 (Lean.Doc.Block.ol start items)) →
                              ((items : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                  motive_3 items → motive_1 (Lean.Doc.Block.dl items)) →
                                ((items : Array (Lean.Doc.Block i b)) →
                                    motive_4 items → motive_1 (Lean.Doc.Block.blockquote items)) →
                                  ((content : Array (Lean.Doc.Block i b)) →
                                      motive_4 content → motive_1 (Lean.Doc.Block.concat content)) →
                                    ((container : b) →
                                        (content : Array (Lean.Doc.Block i b)) →
                                          motive_4 content → motive_1 (Lean.Doc.Block.other container content)) →
                                      ((toList : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                          motive_5 toList → motive_2 { toList := toList }) →
                                        ((toList : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                            motive_6 toList → motive_3 { toList := toList }) →
                                          ((toList : List (Lean.Doc.Block i b)) →
                                              motive_7 toList → motive_4 { toList := toList }) →
                                            motive_5 [] →
                                              ((head : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                                  (tail : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                                    motive_8 head → motive_5 tail → motive_5 (head :: tail)) →
                                                motive_6 [] →
                                                  ((head : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                                      (tail :
                                                          List
                                                            (Lean.Doc.DescItem (Lean.Doc.Inline i)
                                                              (Lean.Doc.Block i b))) →
                                                        motive_9 head → motive_6 tail → motive_6 (head :: tail)) →
                                                    motive_7 [] →
                                                      ((head : Lean.Doc.Block i b) →
                                                          (tail : List (Lean.Doc.Block i b)) →
                                                            motive_1 head → motive_7 tail → motive_7 (head :: tail)) →
                                                        ((contents : Array (Lean.Doc.Block i b)) →
                                                            motive_4 contents → motive_8 { contents := contents }) →
                                                          ((term : Array (Lean.Doc.Inline i)) →
                                                              (desc : Array (Lean.Doc.Block i b)) →
                                                                motive_4 desc →
                                                                  motive_9 { term := term, desc := desc }) →
                                                            (t :
                                                                List
                                                                  (Lean.Doc.DescItem (Lean.Doc.Inline i)
                                                                    (Lean.Doc.Block i b))) →
                                                              motive_6 t