{α : Type} →
  {motive : Aesop.Script.LazyStep.BuildInput α → Sort u} →
    (t : Aesop.Script.LazyStep.BuildInput α) →
      ((tac : Lean.MetaM α) →
          (postGoals : α → Array Lean.MVarId) →
            (tacticBuilder : α → Aesop.Script.TacticBuilder) →
              motive { tac := tac, postGoals := postGoals, tacticBuilder := tacticBuilder }) →
        motive t