∀ {α : Type v} [inst : DecidableEq α] {ι : Type u} {t : ι → Finset α} {s : Finset ι},
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∀ (s' : Finset ↑↑s), s'.card ≤ (s'.biUnion fun a' => t ↑a').card