proposition: Lemma iota_imp_constructive_definite_description : IotaStatement -> ConstructiveDefiniteDescription.
proof: Proof. intros D_iota A P H. destruct D_iota with (P:=P) as (x,H1). - destruct H; red in H; auto. - exists x; apply H1; assumption. Qed.
imports: RelationClasses Logic