proposition: Lemma finite_dep_choice: forall (A:Type) (B:forall x:A, Type) (R:forall x:A, B x->Prop), FiniteT A -> (forall x:A, exists y:B x, R x y) -> exists f:(forall x:A, B x), forall x:A, R x (f x).
proof: Proof. intros. revert B R H0. induction H. - intros. exists (fun x:False => False_rect (B x) x). destruct x. - intros. pose proof (IHFiniteT (fun x:T => B (Some x)) (fun x:T => R (Some x)) (fun x:T => H0 (Some x))). destruct H1. pose proof (H0 None). destruct H2. exists (fun y:option T => match y return (B y) with | Some y0 => x y0 | None => x0 end). destruct x1; auto. - intros. destruct H0. pose proof (IHFiniteT (fun x:X => B (f x)) (fun x:X => R (f x)) (fun x:X => H1 (f x))). destruct H3. unshelve eexists. + intros. rewrite <- H2. apply x. + intros. simpl. rewrite <- (H2 x0). simpl. apply H3. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)