{motive_1 : Aesop.Script.StepTree → Sort u} →
  {motive_2 : Array Aesop.Script.StepTree → Sort u} →
    {motive_3 : List Aesop.Script.StepTree → Sort u} →
      motive_1 Aesop.Script.StepTree.empty →
        ((step : Aesop.Script.Step) →
            (index : ℕ) →
              (children : Array Aesop.Script.StepTree) →
                motive_2 children → motive_1 (Aesop.Script.StepTree.node step index children)) →
          ((toList : List Aesop.Script.StepTree) → motive_3 toList → motive_2 { toList := toList }) →
            motive_3 [] →
              ((head : Aesop.Script.StepTree) →
                  (tail : List Aesop.Script.StepTree) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                (t : Array Aesop.Script.StepTree) → motive_2 t