proposition: Theorem functional_choice_to_inhabited_forall_commute : FunctionalChoice -> InhabitedForallCommute.
proof: Proof. intros choose0 A B Hinhab. pose proof (non_dep_dep_functional_choice choose0) as choose;clear choose0. assert (Hexists : forall x, exists _ : B x, True). { intros x;apply inhabited_sig_to_exists. refine (inhabited_covariant _ (Hinhab x)). intros y;exists y;exact I. } apply choose in Hexists. destruct Hexists as [f _]. exact (inhabits f). Qed.
imports: RelationClasses Logic Wf_nat Decidable