proposition: Lemma finite_choice : forall (A B:Type) (R:A->B->Prop), FiniteT A -> (forall x:A, exists y:B, R x y) -> exists f:A->B, forall x:A, R x (f x).
proof: Proof. intros. apply finite_dep_choice; assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)