{motive : Aesop.Script.StaticStructureM.Context → Sort u} →
  (t : Aesop.Script.StaticStructureM.Context) →
    ((steps : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step)) → motive { steps := steps }) → motive t