{motive : Aesop.Script.SScript → Sort u} →
  (t : Aesop.Script.SScript) →
    t.ctorIdx = 1 →
      ((goalPos : ℕ) →
          (step : Aesop.Script.Step) →
            (tail : Aesop.Script.SScript) → motive (Aesop.Script.SScript.onGoal goalPos step tail)) →
        motive t