proposition: Lemma dependent_functional_choice : forall A (B:A->Type) (R:forall x, B x -> Prop), (forall x, exists y, R x y) -> (exists f, forall x, R x (f x)).
proof: Proof. Proof using. introv H. pose (B' := { x:A & B x }). pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). destruct (functional_choice R') as (f,Hf). intros x. destruct (H x) as (y,Hy). exists (existT (fun x => B x) x y). split~. sets proj1_transparent: (fun P Q (p:P/\Q) => let (a,b) := p in a). exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_transparent _ _ (Hf x))). intros x. destruct (Hf x) as (Heq,HR) using and_indd. destruct (f x). simpls. destruct Heq using eq_indd. apply HR. Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)