{motive : Aesop.CasesTarget → Sort u} →
  (t : Aesop.CasesTarget) →
    ((decl : Lean.Name) → motive (Aesop.CasesTarget.decl decl)) →
      ((patterns : Array Aesop.CasesPattern) → motive (Aesop.CasesTarget.patterns patterns)) → motive t