{α : Type} →
  (motive : α × Aesop.Script.TacticState → Sort u_1) →
    (__discr : α × Aesop.Script.TacticState) →
      ((a : α) → (postTs : Aesop.Script.TacticState) → motive (a, postTs)) → motive __discr