The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Cedric Auger 
>>>>> <sedrikov AT gmail.com>
>>>>>  writes:

> ​I am sorry to have mentionned Empty_set for the base case. I meant "unit"
> (and you do not require the "S O" case, as "prod A unit" is isomorphic to
> "A").​

Yes, I worked this out later today. :)

Another benefit of this approach is that I was able to make all use of vector
and fin disappear from the extracted Haskell code, where it now reduces down
to Int and [a], so cheers all around.

Emilio's suggestion about using ssreflect tuples is a great one -- since I'm
trying to use ssreflect more; I will investigate that avenue next.

John