proposition: Lemma constructive_definite_description : forall (A : Type) (P : A->Prop), (exists! x, P x) -> { x : A | P x }.
proof: Proof. apply iota_imp_constructive_definite_description. exact iota_statement. Qed.
imports: ChoiceFacts