proposition: Lemma constructive_indefinite_description : forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }.
proof: Proof. apply epsilon_imp_constructive_indefinite_description. exact epsilon_statement. Qed.
imports: ChoiceFacts