proposition: Theorem classical_indefinite_description : forall (A : Type) (P : A->Prop), inhabited A -> { x : A | (exists x, P x) -> P x }.
proof: Proof. intros A P i. destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP]. - apply constructive_indefinite_description with (P:= fun x => (exists x, P x) -> P x). destruct Hex as (x,Hx). exists x; intros _; exact Hx. - assert {x : A | True} as (a,_). { apply constructive_indefinite_description with (P := fun _ : A => True). destruct i as (a); firstorder. } firstorder. Defined.
imports: Classical ChoiceFacts