{motive_1 : Aesop.Script.StepTree → Sort u} →
  (t : Aesop.Script.StepTree) →
    t.ctorIdx = 1 →
      ((step : Aesop.Script.Step) →
          (index : ℕ) →
            (children : Array Aesop.Script.StepTree) → motive_1 (Aesop.Script.StepTree.node step index children)) →
        motive_1 t