proposition: Theorem functional_dependent_choice_imp_functional_countable_choice : FunctionalDependentChoice -> FunctionalCountableChoice.
proof: Proof. intros H A R H0. set (R' (p q:nat*A) := fst q = S (fst p) /\ R (fst p) (snd q)). destruct (H0 0) as (y0,Hy0). destruct H with (R:=R') (x0:=(0,y0)) as (f,(Hf0,HfS)). - intro x; destruct (H0 (fst x)) as (y,Hy). exists (S (fst x),y). red. auto. - assert (Heq:forall n, fst (f n) = n). + induction n. * rewrite Hf0; reflexivity. * specialize HfS with n; destruct HfS as (->,_); congruence. + exists (fun n => snd (f (S n))). intro n'. specialize HfS with n'. destruct HfS as (_,HR). rewrite Heq in HR. assumption. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith