Set Asymmetric Patterns.
Require Import ClassicalChoice.

Lemma choice_on_dependent_type: ∀ {A:Type} {B:A→Type}
  (R:∀ a:A, B a → Prop),
  (∀ a:A, ∃ b:B a, R a b) →
  ∃ f:(∀ a:A, B a), ∀ a:A, R a (f a).
Proof.
intros.
destruct (choice (fun (a:A) (b:{a:A & B a}) ⇒
  match b with existT a' b0 ⇒ a=a' ∧ R a' b0 end))
as [choice_fun].
intro a.
destruct (H a) as [b].
∃ (existT (fun a:A ⇒ B a) a b).
split; trivial.
assert (f0:∀ a:A, {b:B a | R a b}).
intro.
pose proof (H0 a).
destruct (choice_fun a) as [a' b].
destruct H1.
destruct H1.
∃ b; trivial.
∃ (fun a:A ⇒ proj1_sig (f0 a)).
intro.
destruct (f0 a) as [b].
exact r.
Qed.