The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

Thanks a lot - it does work indeed! And this typo proves that humans and not 
Coq are the usual suspects :-)

The most interesting challenge now is to prove that the borrowedS and 
borrowedP successor/predecessor functions are equivalent to sT and pT. 

I was wondering if anyone has seen papers about taking advantage of the 
presence of a bijection between some trickier data type and "nat" to somewhat 
automate the proof of computations or properties borrowed from "nat" using 
the bijection. Or papers about automation of structural recursion 
requirements in the presence of such a bijection.

Paul

On Jun 27, 2011, at 1:27 PM, 
brandon_m_moore AT yahoo.com
 wrote:

> The code seems to work correctly after replacing
> 
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C _ y =>y
> end.
> 
> by
> 
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C x _ =>x
> end.