Section TTDiaconescu.

Definition EquivRel (A : Set) (R : AAProp) :=
( x : A, R x x)
( x y : A, R x yR y x)
( x y z : A, R x yR y zR x z).

Definition Tchoice :=
(A : Set) (R : AAProp),
EquivRel A R
ex
(fun f : AA
( x : A, R x (f x)) ( x y : A, R x yf x = f y)).

Hypothesis TTCA : Tchoice.

Hypothesis P : Prop.

Inductive rel : boolboolProp :=
| rrefl : b : bool, rel b b
| rel2 : b c : bool, Prel b c.

Hint Resolve rrefl rel2.

Lemma rel_trans : x y z : bool, rel x yrel y zrel x z.
intros x y z h1; inversion h1; auto.
Qed.

Lemma rel_sym : x y : bool, rel x yrel y x.
intros x y h; inversion h; auto.
Qed.

Hint Resolve rel_sym rel_trans.

Lemma rel_equiv : EquivRel bool rel.
split; auto; split; intros; eauto.
Qed.

Lemma eq_bool_dec : a b : bool, a = b a b.
simple induction a; simple induction b; auto; try (right; discriminate).
Qed.

Theorem EM : P ¬ P.

elim (TTCA bool rel rel_equiv).
intros f; simple induction 1; intros hf1 hf2.

elim (eq_bool_dec (f true) (f false)); intros h.

cut (rel true false).
intros hr; inversion hr; auto.
apply rel_trans with (f true); auto.

rewrite h.
apply rel_sym; auto.

right; unfold not in |- *; intros p.
apply h.
apply hf2.
auto.

Qed.

End TTDiaconescu.

Inductive EXType (A : Type) (P : AProp) : Prop :=
EXi : a : A, P aEXType A P.

Section TTDiaconescu2.

Definition Tchoice2 :=
(A : Set) (R : AAProp),
EquivRel A R
EXType (AProp)
(fun P : AProp
( x : A, ex (fun y : AR x y P y))
( x y : A, R x yP xP yx = y)).

Hypothesis TTAC2 : Tchoice2.

Hypothesis P : Prop.

Definition rel' := rel P.

Hint Resolve rel2.

Lemma EM2 : P ¬ P.
elim (TTAC2 bool rel' (rel_equiv P)).
intro Q; simple induction 1; intros hQ1 hQ2.
elim (hQ1 true); intros w_true; simple induction 1; intros ht1 ht2.
elim (hQ1 false); intros w_false; simple induction 1; intros hf1 hf2.
elim (eq_bool_dec w_true w_false); intro e.
left; cut (rel' true false).
intro hr; inversion hr; auto.
unfold rel' in |- *; apply rel_trans with w_true; auto.
apply rel_sym; rewrite e; auto.
right; unfold not in |- *; intro p; apply e; auto.
apply hQ2; auto.
unfold rel' in |- *; auto.
Qed.

End TTDiaconescu2.