∀ {α : Type u_2} {ι' : Sort u_1} {p' : ι' → Prop} {s' : ι' → Set α} (t : Set α) (motive : (∃ i, p' i ∧ s' i ⊆ t) → Prop)
  (x : ∃ i, p' i ∧ s' i ⊆ t), (∀ (i' : ι') (hi' : p' i') (ht : s' i' ⊆ t), motive ⋯) → motive x