Library CoLoR.Util.Logic.DepChoice
CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
Frederic Blanqui, 2007-08-08
dependent choice axiom
Set Implicit Arguments
.
Axiom
dep_choice
:
forall
(
A
:
Type
) (
a
:
A
) (
R
:
relation
A
),
classic_left_total
R
->
exists
f
,
IS
R
f
/\
f
0
=
a
.