proposition: Lemma finite_choice `{Finite A} {B : A → Type} (P : ∀ x, B x → Prop) : (∀ x, ∃ y, P x y) → ∃ f, ∀ x, P x (f x).
proof: Proof. intros Hex. destruct (fin_choice _ (λ i, Hex (decode_fin i))) as [f ?]. exists (λ x, eq_rect _ _ (f(encode_fin x)) _ (decode_encode_fin x)); intros x. destruct (decode_encode_fin x); simpl; auto. Qed.
imports: stdpp(options)