{α : Type u_1} →
  {s : Set α} →
    {motive : s.FiniteExhaustion → Sort u} →
      ((toFun : ℕ → Set α) →
          (finite' : ∀ (n : ℕ), Finite ↑(toFun n)) →
            (subset_succ' : ∀ (n : ℕ), toFun n ⊆ toFun (n + 1)) →
              (iUnion_eq' : ⋃ n, toFun n = s) →
                motive { toFun := toFun, finite' := finite', subset_succ' := subset_succ', iUnion_eq' := iUnion_eq' }) →
        (t : s.FiniteExhaustion) → motive t