{motive : Aesop.Script.DynStructureResult → Sort u} →
  (t : Aesop.Script.DynStructureResult) →
    ((script : List Aesop.Script.Step) →
        (postState : Lean.Meta.SavedState) → motive { script := script, postState := postState }) →
      motive t