{motive : Aesop.ExtResult → Sort u} →
  ((depth : ℕ) →
      (commonFVarIds : Array Lean.FVarId) →
        (goals : Array (Lean.MVarId × Array Lean.FVarId)) →
          motive { depth := depth, commonFVarIds := commonFVarIds, goals := goals }) →
    (t : Aesop.ExtResult) → motive t