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