{motive : Aesop.GoalStats → Sort u} →
  ((goalId : ℕ) →
      (goalKind : Aesop.GoalKind) →
        (lctxSize depth : ℕ) →
          (forwardStateStats : Aesop.ForwardStateStats) →
            motive
              { goalId := goalId, goalKind := goalKind, lctxSize := lctxSize, depth := depth,
                forwardStateStats := forwardStateStats }) →
    (t : Aesop.GoalStats) → motive t