The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Lisa,

  You may have a look at the module Logic.ClassicalEpsilon, which 
allows you to use Hilbert's Choice operator.

Best,

Pierre


> Do you mean that we could use "choice_axiom" to handle the "exists" so that 
> the
> proof can go on? If we take (trace->trace) for A and trace for B, how can we
> construct R?
> Axiom choice_axiom:forall (A B : Type) (R : A->B->Prop),
>     (forall x : A, exists y : B, R x y) ->
>      exists f : A->B, (forall x : A, R x (f x)).
> Thank you very much!