∀ {β α : Type u} {s : Set β} (f : ↑s → α),
  ∀ θ ≤ Cardinal.mk ↑s,
    Cardinal.aleph0 ≤ θ →
      Cardinal.mk α < θ.ord.cof → ∃ a t, ∃ (h : t ⊆ s), θ ≤ Cardinal.mk ↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a