proposition: Lemma informative_or_lift : forall P Q : Prop, P \/ Q -> {P} + {Q}.
proof: Proof. intros P Q. assert ({P} + {~P}) as H by (apply excluded_middle_informative). destruct H. * intro. left. exact p. * intros H. assert ({Q} + {~Q}) as H2 by (apply excluded_middle_informative). destruct H2. + right. exact q. + assert (~~Q). { destruct H. + contradiction. + intro H1. destruct H1. exact H. } contradiction. Qed.
imports: ClassicalEpsilon