proposition: Theorem dep_non_dep_functional_choice : DependentFunctionalChoice -> FunctionalChoice.
proof: Proof. intros AC_depfun A B R H. destruct (AC_depfun A (fun _ => B) R H) as (f,Hf). exists f; trivial. Qed.
imports: RelationClasses Logic Wf_nat Decidable