proposition: Theorem functional_choice_imp_functional_dependent_choice : FunctionalChoice -> FunctionalDependentChoice.
proof: Proof. intros FunChoice A R HRfun x0. apply FunChoice in HRfun as (g,Rg). set (f:=fix f n := match n with 0 => x0 | S n' => g (f n') end). exists f; firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith