indefinite description equivalent to simple description

simple_description.v

(* https://coq.discourse.group/t/indefinite-description-axiom-could-be-simpler/1764 *)
 
From Coq Require Import ssreflect ssrbool ssrfun.

Definition indefinite_description :=
  forall (A : Type) (P : A->Prop), ex P -> sig P.

Definition simple_description :=
  forall (A : Type), inhabited A -> A.

Proposition simple_description_implies_indefinite_description :
  simple_description -> indefinite_description.
Proof.
move=>H A P Hx.
by apply: H; case: Hx=>x Px; constructor; exists x.
Qed.

Proposition indefinite_description_implies_simple_description :
  indefinite_description -> simple_description.
Proof.
move=>H A Ha.
apply: (proj1_sig (P:=fun=>True)).
by apply: H; case: Ha=>a; exists a.
Qed.