proposition: Theorem inhabited_forall_commute_to_functional_choice : InhabitedForallCommute -> FunctionalChoice.
proof: Proof. intros choose A B R Hexists. assert (Hinhab : forall x, inhabited {y : B | R x y}). { intros x;apply exists_to_inhabited_sig;trivial. } apply choose in Hinhab. destruct Hinhab as [f]. exists (fun x => proj1_sig (f x)). exact (fun x => proj2_sig (f x)). Qed.
imports: RelationClasses Logic Wf_nat Decidable