proposition: Lemma epsilon_imp_constructive_indefinite_description: EpsilonStatement -> ConstructiveIndefiniteDescription.
proof: Proof. intros D_epsilon A P H. destruct D_epsilon with (P:=P) as (x,H1). - destruct H; auto. - exists x; apply H1; assumption. Qed.
imports: RelationClasses Logic