Library hilbert.BadEpsilon2

Definition inhabited (A:Type) := exists a:A, True.

Parameter epsilon : forall A:Type,
         inhabited A -> (A ->Prop) -> A.

Section or_to_sumbool.
 Variables P Q:Prop.

 Hypothesis P_or_Q : P \/ Q.

 Definition or_sumbool : {P}+{Q}.
 refine (epsilon ({P}+{Q}) _ (fun _ => True)).
 case P_or_Q; intro H;
   [ exists (left Q H) | exists (right P H)];
   trivial.
 Defined.
End or_to_sumbool.

Section exists_to_sigT.
 Variable A : Type.
 Variable P : A-> Prop.
 Hypothesis ex : exists a:A, P a.

 Definition exists_sigT : sigT P.
 refine (epsilon (sigT P) _ (fun _ => True)).
 case ex;intros a Ha.
 exists (existT P a Ha);trivial.
 Defined.

End exists_to_sigT.