Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails Excluded-Middle in Type Theory [LacasWerner99].

Three variants of Diaconescu's result in type theory are shown below.

A. A proof that the relational form of the Axiom of Choice + Extensionality for Predicates entails Excluded-Middle (by Hugo Herbelin)

B. A proof that the relational form of the Axiom of Choice + Proof Irrelevance entails Excluded-Middle for Equality Statements (by Benjamin Werner)

C. A proof that extensional Hilbert epsilon's description operator entails excluded-middle (taken from Bell [Bell93])

See also [Carlström04] for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle

[Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, in Proceedings of AMS, vol 51, pp 176-178, 1975.

[LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999.

[Bell93] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993

[Carlström04] Jesper Carlström, EM + Ext + AC_int is equivalent to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.

Require ClassicalFacts ChoiceFacts.

(**********************************************************************)

Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle

Section PredExt_RelChoice_imp_EM.

The axiom of extensionality for predicates

Definition PredicateExtensionality :=
  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.

From predicate extensionality we get propositional extensionality hence proof-irrelevance

Import ClassicalFacts.

Variable pred_extensionality : PredicateExtensionality.

Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.pred_extensionality:PredicateExtensionality
forall A B : Prop, A <-> B -> A = B
Proof.pred_extensionality:PredicateExtensionality
forall A B : Prop, A <-> B -> A = B
  intros A B H.pred_extensionality:PredicateExtensionality
A, B:Prop
H:A <-> B
A = B
  change ((fun _ => A) true = (fun _ => B) true).pred_extensionality:PredicateExtensionality
A, B:Prop
H:A <-> B
(fun _ : bool => A) true = (fun _ : bool => B) true
  rewrite
   pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).pred_extensionality:PredicateExtensionality
A, B:Prop
H:A <-> B
B = B
pred_extensionality:PredicateExtensionality
A, B:Prop
H:A <-> B
bool -> A <-> B
    reflexivity.pred_extensionality:PredicateExtensionality
A, B:Prop
H:A <-> B
bool -> A <-> B
    intros _; exact H.
Qed.

Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.pred_extensionality:PredicateExtensionality
forall (A : Prop) (a1 a2 : A), a1 = a2
Proof.pred_extensionality:PredicateExtensionality
forall (A : Prop) (a1 a2 : A), a1 = a2
  apply (ext_prop_dep_proof_irrel_cic prop_ext).
Qed.

From proof-irrelevance and relational choice, we get guarded relational choice

Import ChoiceFacts.

Variable rel_choice : RelationalChoice.

Lemma guarded_rel_choice : GuardedRelationalChoice.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
GuardedRelationalChoice
Proof.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
GuardedRelationalChoice
 apply
  (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
Qed.

The form of choice we need: there is a functional relation which chooses an element in any non empty subset of bool

Import Bool.

Lemma AC_bool_subset_to_bool :
  exists R : (bool -> Prop) -> bool -> Prop,
   (forall P:bool -> Prop,
      (exists b : bool, P b) ->
       exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
exists R : (bool -> Prop) -> bool -> Prop,
  forall P : bool -> Prop,
  (exists b : bool, P b) ->
  exists b : bool,
    P b /\
    R P b /\ (forall b' : bool, R P b' -> b = b')
Proof.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
exists R : (bool -> Prop) -> bool -> Prop,
  forall P : bool -> Prop,
  (exists b : bool, P b) ->
  exists b : bool,
    P b /\
    R P b /\ (forall b' : bool, R P b' -> b = b')
  destruct (guarded_rel_choice _ _
   (fun Q:bool -> Prop =>  exists y : _, Q y)
   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
forall x : bool -> Prop,
(exists y : bool, x y) -> exists y : bool, x y
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
R:(bool -> Prop) -> bool -> Prop
HRsub:subrelation R
  (fun (Q : bool -> Prop) (y : bool) => Q y)
HR:forall x : bool -> Prop,
(exists y : bool, x y) ->
exists ! y : bool, R x y
exists R0 : (bool -> Prop) -> bool -> Prop,
  forall P : bool -> Prop,
  (exists b : bool, P b) ->
  exists b : bool,
    P b /\
    R0 P b /\ (forall b' : bool, R0 P b' -> b = b') 
    exact (fun _ H => H).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
R:(bool -> Prop) -> bool -> Prop
HRsub:subrelation R
  (fun (Q : bool -> Prop) (y : bool) => Q y)
HR:forall x : bool -> Prop,
(exists y : bool, x y) ->
exists ! y : bool, R x y
exists R0 : (bool -> Prop) -> bool -> Prop,
  forall P : bool -> Prop,
  (exists b : bool, P b) ->
  exists b : bool,
    P b /\
    R0 P b /\ (forall b' : bool, R0 P b' -> b = b')
  exists R; intros P HP.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
R:(bool -> Prop) -> bool -> Prop
HRsub:subrelation R
  (fun (Q : bool -> Prop) (y : bool) => Q y)
HR:forall x : bool -> Prop,
(exists y : bool, x y) ->
exists ! y : bool, R x y
P:bool -> Prop
HP:exists b : bool, P b
exists b : bool,
  P b /\ R P b /\ (forall b' : bool, R P b' -> b = b')
  destruct (HR P HP) as (y,(Hy,Huni)).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
R:(bool -> Prop) -> bool -> Prop
HRsub:subrelation R
  (fun (Q : bool -> Prop) (y0 : bool) => Q y0)
HR:forall x : bool -> Prop,
(exists y0 : bool, x y0) ->
exists ! y0 : bool, R x y0
P:bool -> Prop
HP:exists b : bool, P b
y:bool
Hy:R P y
Huni:forall x' : bool, R P x' -> y = x'
exists b : bool,
  P b /\ R P b /\ (forall b' : bool, R P b' -> b = b')
  exists y; firstorder.
Qed.

The proof of the excluded middle

Remark: P could have been in Set or Type

Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
forall P : Prop, P \/ ~ P
Proof.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
forall P : Prop, P \/ ~ P
intro P.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
P \/ ~ P

(* first we exhibit the choice functional relation R *)
destruct AC_bool_subset_to_bool as [R H].pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
P \/ ~ P

set (class_of_true := fun b => b = true \/ P).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
P \/ ~ P
set (class_of_false := fun b => b = false \/ P).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
P \/ ~ P

(* the actual "decision": is (R class_of_true) = true or false? *)
destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
exists b : bool, class_of_true b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:class_of_true b0
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
exists true; left; reflexivity.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:class_of_true b0
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
destruct H0.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P

(* the actual "decision": is (R class_of_false) = true or false? *)
destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
exists b : bool, class_of_false b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:class_of_false b1
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
exists false; left; reflexivity.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:class_of_false b1
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
destruct H1.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P

(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
right.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
intro HP.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
forall b : bool, class_of_true b <-> class_of_false b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
intro b; split.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b2 : bool, P0 b2) ->
exists b2 : bool,
  P0 b2 /\
  R P0 b2 /\
  (forall b' : bool, R P0 b' -> b2 = b')
class_of_true:=fun b2 : bool => b2 = true \/ P:bool -> Prop
class_of_false:=fun b2 : bool => b2 = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
b:bool
class_of_true b -> class_of_false b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b2 : bool, P0 b2) ->
exists b2 : bool,
  P0 b2 /\
  R P0 b2 /\
  (forall b' : bool, R P0 b' -> b2 = b')
class_of_true:=fun b2 : bool => b2 = true \/ P:bool -> Prop
class_of_false:=fun b2 : bool => b2 = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
b:bool
class_of_false b -> class_of_true b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
unfold class_of_false; right; assumption.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b2 : bool, P0 b2) ->
exists b2 : bool,
  P0 b2 /\
  R P0 b2 /\
  (forall b' : bool, R P0 b' -> b2 = b')
class_of_true:=fun b2 : bool => b2 = true \/ P:bool -> Prop
class_of_false:=fun b2 : bool => b2 = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
b:bool
class_of_false b -> class_of_true b
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
unfold class_of_true; right; assumption.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
assert (Heq : class_of_true = class_of_false).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
class_of_true = class_of_false
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
apply pred_extensionality with (1 := Hequiv).pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
False
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
apply diff_true_false.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
true = false
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
rewrite <- H0.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
b0 = false
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
rewrite <- H1.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
b0 = b1
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
rewrite <- H0''.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
b0 = b0
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
R class_of_true b1
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P reflexivity.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
R class_of_true b1
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
rewrite Heq.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:b1 = false
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
HP:P
Hequiv:forall b : bool,
class_of_true b <-> class_of_false b
Heq:class_of_true = class_of_false
R class_of_false b1
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
assumption.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:b0 = true
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
b1:bool
H1:P
H1':R class_of_false b1
H1'':forall b' : bool,
R class_of_false b' -> b1 = b'
P \/ ~ P
pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P

(* cases where P is true *)
left; assumption.pred_extensionality:PredicateExtensionality
rel_choice:RelationalChoice
P:Prop
R:(bool -> Prop) -> bool -> Prop
H:forall P0 : bool -> Prop,
(exists b : bool, P0 b) ->
exists b : bool,
  P0 b /\
  R P0 b /\ (forall b' : bool, R P0 b' -> b = b')
class_of_true:=fun b : bool => b = true \/ P:bool -> Prop
class_of_false:=fun b : bool => b = false \/ P:bool -> Prop
b0:bool
H0:P
H0':R class_of_true b0
H0'':forall b' : bool, R class_of_true b' -> b0 = b'
P \/ ~ P
left; assumption.

Qed.

End PredExt_RelChoice_imp_EM.

(**********************************************************************)

Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality

This is an adaptation of Diaconescu's theorem, exploiting the form of extensionality provided by proof-irrelevance

Section ProofIrrel_RelChoice_imp_EqEM.

Import ChoiceFacts.

Variable rel_choice : RelationalChoice.

Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.

Let a1 and a2 be two elements in some type A

Variable A :Type.
Variables a1 a2 : A.

We build the subset A' of A made of a1 and a2

Definition A' := @sigT A (fun x => x=a1 \/ x=a2).

Definition a1':A'.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
A'
exists a1 ; auto.
Defined.

Definition a2':A'.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
A'
exists a2 ; auto.
Defined.

By proof-irrelevance, projection is a retraction

Lemma projT1_injective : a1=a2 -> a1'=a2'.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 -> a1' = a2'
Proof.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 -> a1' = a2'
  intro Heq ; unfold a1', a2', A'.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
Heq:a1 = a2
existT (fun x : A => x = a1 \/ x = a2) a1
  (or_introl eq_refl) =
existT (fun x : A => x = a1 \/ x = a2) a2
  (or_intror eq_refl)
  rewrite Heq.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
Heq:a1 = a2
existT (fun x : A => x = a2 \/ x = a2) a2
  (or_introl eq_refl) =
existT (fun x : A => x = a2 \/ x = a2) a2
  (or_intror eq_refl)
  replace (or_introl (a2=a2) (eq_refl a2))
     with (or_intror (a2=a2) (eq_refl a2)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
Heq:a1 = a2
existT (fun x : A => x = a2 \/ x = a2) a2
  (or_intror eq_refl) =
existT (fun x : A => x = a2 \/ x = a2) a2
  (or_intror eq_refl)
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
Heq:a1 = a2
or_intror eq_refl = or_introl eq_refl
  reflexivity.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
Heq:a1 = a2
or_intror eq_refl = or_introl eq_refl
  apply proof_irrelevance.
Qed.

But from the actual proofs of being in A', we can assert in the proof-irrelevant world the existence of relevant boolean witnesses

Lemma decide : forall x:A', exists y:bool ,
  (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
forall x : A',
exists y : bool,
  projT1 x = a1 /\ y = true \/
  projT1 x = a2 /\ y = false
Proof.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
forall x : A',
exists y : bool,
  projT1 x = a1 /\ y = true \/
  projT1 x = a2 /\ y = false
  intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.
Qed.

Thanks to the axiom of choice, the boolean witnesses move from the propositional world to the relevant world

Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 \/ a1 <> a2
Proof.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 \/ a1 <> a2
  destruct
    (rel_choice A' bool
       (fun x y =>  projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))
    as (R,(HRsub,HR)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
forall x : A',
exists y : bool,
  projT1 x = a1 /\ y = true \/
  projT1 x = a2 /\ y = false
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
a1 = a2 \/ a1 <> a2
    apply decide.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
a1 = a2 \/ a1 <> a2
  destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
a1 = a2 \/ a1 <> a2
  destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  destruct (HR a2') as (b2,(Ha2'b2,Huni2)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2'b2:R a2' b2
Huni2:forall x' : bool, R a2' x' -> b2 = x'
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2'b2:R a2' b2
Huni2:forall x' : bool, R a2' x' -> b2 = x'
Ha2a1:projT1 a2' = a1
_Hb2true:b2 = true
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2'b2:R a2' b2
Huni2:forall x' : bool, R a2' x' -> b2 = x'
Hb2false:b2 = false
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    left; symmetry; assumption.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2'b2:R a2' b2
Huni2:forall x' : bool, R a2' x' -> b2 = x'
Hb2false:b2 = false
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    right; intro H.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2'b2:R a2' b2
Huni2:forall x' : bool, R a2' x' -> b2 = x'
Hb2false:b2 = false
H:a1 = a2
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    subst b1; subst b2.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
_Huni1:forall x' : bool, R a1' x' -> true = x'
Ha1'b1:R a1' true
Huni2:forall x' : bool, R a2' x' -> false = x'
Ha2'b2:R a2' false
H:a1 = a2
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    rewrite (projT1_injective H) in Ha1'b1.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
_Huni1:forall x' : bool, R a1' x' -> true = x'
Ha1'b1:R a2' true
Huni2:forall x' : bool, R a2' x' -> false = x'
Ha2'b2:R a2' false
H:a1 = a2
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    assert (false = true) by auto using Huni2.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
_Huni1:forall x' : bool, R a1' x' -> true = x'
Ha1'b1:R a2' true
Huni2:forall x' : bool, R a2' x' -> false = x'
Ha2'b2:R a2' false
H:a1 = a2
H0:false = true
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    discriminate.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
R:A' -> bool -> Prop
HRsub:subrelation R
  (fun (x : A') (y : bool) =>
   projT1 x = a1 /\ y = true \/
   projT1 x = a2 /\ y = false)
HR:forall x : A', exists ! y : bool, R x y
b1:bool
Ha1'b1:R a1' b1
_Huni1:forall x' : bool, R a1' x' -> b1 = x'
Ha1a2:projT1 a1' = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  left; assumption.
Qed.

An alternative more concise proof can be done by directly using the guarded relational choice

Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 \/ a1 <> a2
Proof.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
a1 = a2 \/ a1 <> a2
  assert (decide: forall x:A, x=a1 \/ x=a2 ->
                exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
a1 = a2 \/ a1 <> a2
    intros a [Ha1|Ha2]; [exists true | exists false]; auto.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
a1 = a2 \/ a1 <> a2
  assert (guarded_rel_choice :=
          rel_choice_and_proof_irrel_imp_guarded_rel_choice
	  rel_choice
	  proof_irrelevance).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
a1 = a2 \/ a1 <> a2
  destruct
    (guarded_rel_choice A bool
      (fun x => x=a1 \/ x=a2)
      (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))
      as (R,(HRsub,HR)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
a1 = a2 \/ a1 <> a2
      apply decide.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
a1 = a2 \/ a1 <> a2
  destruct (HR a1) as (b1,(Ha1b1,_Huni1)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
a1 = a1 \/ a1 = a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
a1 = a2 \/ a1 <> a2 left; reflexivity.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
a1 = a2 \/ a1 <> a2
  destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  destruct (HR a2) as (b2,(Ha2b2,Huni2)).rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
a2 = a1 \/ a2 = a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2 right; reflexivity.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
Ha2a1:a2 = a1
_Hb2true:b2 = true
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
Hb2false:b2 = false
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    left; symmetry; assumption.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
Hb2false:b2 = false
a1 = a2 \/ a1 <> a2
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    right; intro H.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Hb1true:b1 = true
b2:bool
Ha2b2:R a2 b2
Huni2:forall x' : bool, R a2 x' -> b2 = x'
Hb2false:b2 = false
H:a1 = a2
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    subst b1; subst b2; subst a1.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a2:A
decide:forall x : A,
x = a2 \/ x = a2 ->
exists y : bool,
  x = a2 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
Ha1b1:R a2 true
_Huni1:forall x' : bool, R a2 x' -> true = x'
HR:forall x : A,
x = a2 \/ x = a2 -> exists ! y : bool, R x y
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a2 /\ y = true \/ x = a2 /\ y = false)
Huni2:forall x' : bool, R a2 x' -> false = x'
Ha2b2:R a2 false
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    assert (false = true) by auto using Huni2, Ha1b1.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a2:A
decide:forall x : A,
x = a2 \/ x = a2 ->
exists y : bool,
  x = a2 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
Ha1b1:R a2 true
_Huni1:forall x' : bool, R a2 x' -> true = x'
HR:forall x : A,
x = a2 \/ x = a2 -> exists ! y : bool, R x y
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a2 /\ y = true \/ x = a2 /\ y = false)
Huni2:forall x' : bool, R a2 x' -> false = x'
Ha2b2:R a2 false
H:false = true
False
rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
    discriminate.rel_choice:RelationalChoice
proof_irrelevance:forall (P : Prop) (x y : P), x = y
A:Type
a1, a2:A
decide:forall x : A,
x = a1 \/ x = a2 ->
exists y : bool,
  x = a1 /\ y = true \/ x = a2 /\ y = false
guarded_rel_choice:GuardedRelationalChoice
R:A -> bool -> Prop
HRsub:subrelation R
  (fun (x : A) (y : bool) =>
   x = a1 /\ y = true \/ x = a2 /\ y = false)
HR:forall x : A,
x = a1 \/ x = a2 -> exists ! y : bool, R x y
b1:bool
Ha1b1:R a1 b1
_Huni1:forall x' : bool, R a1 x' -> b1 = x'
Ha1a2:a1 = a2
_Hb1false:b1 = false
a1 = a2 \/ a1 <> a2
  left; assumption.
Qed.

End ProofIrrel_RelChoice_imp_EqEM.

(**********************************************************************)

Extensional Hilbert's epsilon description operator -> Excluded-Middle

Proof sketch from Bell [Bell93] (with thanks to P. Castéran)

Notation inhabited A := A (only parsing).

Section ExtensionalEpsilon_imp_EM.

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

Hypothesis epsilon_spec :
  forall (A:Type) (i:inhabited A) (P:A->Prop),
  (exists x, P x) -> P (epsilon A i P).

Hypothesis epsilon_extensionality :
  forall (A:Type) (i:inhabited A) (P Q:A->Prop),
  (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.

Notation eps := (epsilon bool true) (only parsing).

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

End ExtensionalEpsilon_imp_EM.