The Coq mailing list

[Ben <midfield AT gmail.com>]

here are some useful links:

https://sympa.inria.fr/sympa/arc/coq-club/2014-11/msg00124.html
https://gist.github.com/anonymous/e9493ce195219c4c2b18

i tried to do it myself i failed -- i'm just a beginner.  at some point i 
convinced myself that the right way to do it is

- prove pigeonhole for lists of nats (using decidable equality)

- convert the general problem into a problem about lists of nats by using 
indices

but i got bogged down in details.  also there's a Prop vs Type issue with 
appears_in, i think.

best, ben

> On Jan 15, 2015, at 12:14 AM, Jiten Pathy 
> <jpathy AT fssrv.net>
>  wrote:
> 
> 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