The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Taral wrote:
> 
> On Thu, Aug 27, 2009 at 7:54 AM, Celia 
> Picard<celia.picard AT irit.fr>
>  wrote:
>> (* By the way, we have a proof of injectivity of Fin that looks a bit
>> complicated.
>>   Is there a well-known (easier) proof of Fin n = Fin m ->  n = m ? *)
> 
> Not really. Any such proof of type equivalence would necessarily
> involve proving things about the cardinality of Fin n and Fin m by
> example.
> 
> -- 
> Taral 
> <taralx AT gmail.com>
> "Please let me know if there's any further trouble I can give you."
>     -- Unknown
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 


My proof of this Fin injectivity is the culmination of about 500 line script
using pigeonhole principle, I assume you have something similar?
-- 
View this message in context: 
http://www.nabble.com/Mixing-induction-and-coinduction-tp25158409p25178877.html
Sent from the Coq mailing list archive at Nabble.com.