Set Implicit Arguments.
Require Export ClassicalChoice.
Require Import MyTactics.
A version of the axiom of choice, suitable for use at arity 2.
Lemma binary_choice:
forall (
A B :
Type) (
R :
A ->
B ->
B ->
Prop),
(
forall x,
exists y1 y2,
R x y1 y2) ->
exists f1 f2,
forall x,
R x (
f1 x) (
f2 x).
Proof.
introv h.
forwards [
f i ]: (
choice (
fun x (
yy :
B *
B) =>
let (
y1,
y2) :=
yy in R x y1 y2)).
intro x.
destruct (
h x)
as [
y1 [
y2 ? ]].
exists (
y1,
y2).
assumption.
exists (
fun x =>
let (
y1,
y2) :=
f x in y1).
exists (
fun x =>
let (
y1,
y2) :=
f x in y2).
intro x.
specializes i x.
destruct (
f x)
as [
y1 y2 ].
assumption.
Qed.