Load "geuvers-coquand".
Implicit Arguments On.
 
Axiom
   AC :
   (A : Type)
   (B : Type)
   (R : A -> B ->  Prop)
   ((x : A)  (exT B [y : B]  (R x y))) ->
   ((x : A) (y1, y2 : B) (R x y1) -> (R x y2) ->  y1 == y2) ->
    (exT A ->  B [f : A ->  B] (x : A)  (R x (f x))).
 
Axiom EM : (P : Prop)  P \/ ~ P.
 
Tactic Definition CaseEq x :=
 Generalize (refl_eqT ? x); Pattern -1 x; Case x.
 
Lemma existence_decision:
 (!exT ? [f : Prop ->  bool] (P : Prop)  (iff P (f P) == true)).
Apply (!AC ? ? [P : Prop] [b : bool]  (iff P b == true)).
Intros P; Elim (EM P).
Intros p; Exists true; Split; Intuition.
Intros p; Exists false; Split; Intuition.
Inversion H.
Intros x y1 y2.
Elim (EM x).
Intros xx H0 H; Elim H0; Elim H; (Intros; Transitivity true); Intuition.
Case y1; Case y2; Intuition.
Qed.
 
Lemma problem: False.
Generalize existence_decision.
Intros yH.
Elim yH; Intros Prop2bool H; Clear yH.
Cut (P : Prop)  {P}+{~ P}.
Exact par.
Intros P.
Generalize (refl_eqT ? (Prop2bool P)); Pattern -1 (Prop2bool P);
 Case (Prop2bool P).
Intros H0.
Case (H P).
Intros H1 H2.
Left; Exact (H2 H0).
Intros hyp; Right.
Unfold not; Intros p.
Case (H P).
Intros H0 H1.
Rewrite (H0 p) in hyp; Inversion hyp.
Qed.