∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (R : SetRel α β) [inst_1 : (a : α) → Fintype ↑(R.image {a})],
  (∀ (A : Finset α), A.card ≤ Fintype.card ↑(R.image ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), (x, f x) ∈ R