Library Waterproof.Libs.Logic.InformativeEpsilon

Require Import ClassicalEpsilon.

ClassicalEpsilon allows us to lift an uninformative or to an informative or.

Lemma informative_or_lift : forall P Q : Prop, P \/ Q -> {P } + {Q }.
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.