proposition: Lemma exclusive_dec: forall P Q:Prop, ~(P /\ Q) -> (P \/ Q) -> {P} + {Q}.
proof: Proof. intros. assert ({x:bool | if x then P else Q}). { apply constructive_definite_description. case H0. - exists true. red; split. + assumption. + destruct x'. * reflexivity. * tauto. - exists false. red; split. + assumption. + destruct x'. * tauto. * reflexivity. } destruct H1. destruct x; [left|right]; assumption. Qed.
imports: Coq(Description)