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.