{motive_1 : Aesop.IndexingMode → Sort u} →
  {motive_2 : Array Aesop.IndexingMode → Sort u} →
    {motive_3 : List Aesop.IndexingMode → Sort u} →
      motive_1 Aesop.IndexingMode.unindexed →
        ((keys : Array Lean.Meta.DiscrTree.Key) → motive_1 (Aesop.IndexingMode.target keys)) →
          ((keys : Array Lean.Meta.DiscrTree.Key) → motive_1 (Aesop.IndexingMode.hyps keys)) →
            ((imodes : Array Aesop.IndexingMode) → motive_2 imodes → motive_1 (Aesop.IndexingMode.or imodes)) →
              ((toList : List Aesop.IndexingMode) → motive_3 toList → motive_2 { toList := toList }) →
                motive_3 [] →
                  ((head : Aesop.IndexingMode) →
                      (tail : List Aesop.IndexingMode) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                    (t : List Aesop.IndexingMode) → motive_3 t