proposition: Theorem constructive_definite_descr_excluded_middle : (forall A : Type, ConstructiveDefiniteDescription_on A) -> (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
proof: Proof. intros Descr EM P. pose (select := fun b:bool => if b then P else ~P). assert { b:bool | select b } as ([|],HP). - red in Descr. apply Descr. rewrite <- unique_existence; split. + destruct (EM P). * exists true; trivial. * exists false; trivial. + intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction. - left; trivial. - right; trivial. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid