The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

You may find a constructive proof (not using EM but assuming 
decidability of equality on elements) in http://color.inria.fr/ in the 
file Util/List/ListOccur.v . See the file without the proofs in 
http://color.inria.fr/doc/CoLoR.Util.List.ListOccur.html . Hope this can 
help.

Best regards,

Frédéric.

Le 15/01/2015 09:14, Jiten Pathy a écrit :
> Hello,
> Trying to prove pigeon hole from SF using excluded_middle. Stuck while
> doig the following. A hint on what i am doing wrong?
>
> https://gist.github.com/anonymous/548325557388612bd60e