proposition: Lemma constructive_indefinite_descr_fun_choice : ConstructiveIndefiniteDescription -> FunctionalChoice.
proof: Proof. intros IndefDescr A B R H. exists (fun x => proj1_sig (IndefDescr B (R x) (H x))). intro x. apply (proj2_sig (IndefDescr B (R x) (H x))). Qed.
imports: RelationClasses Logic Wf_nat Decidable