proposition: Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
proof: Proof. intro P. pose (B := fun y => y=false \/ P). pose (C := fun y => y=true \/ P). assert (B (eps B)) as [Hfalse|HP] by (apply epsilon_spec; exists false; left; reflexivity). - assert (C (eps C)) as [Htrue|HP] by (apply epsilon_spec; exists true; left; reflexivity). + right; intro HP. assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption). rewrite epsilon_extensionality with (1:=H) in Hfalse. rewrite Htrue in Hfalse. discriminate. + auto. - auto. Qed.