The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> This is a genuine Frequently Asked Question, and it's addressed in Section 
> 3.8 of CPDT: http://adam.chlipala.net/cpdt/

When I searched for the exact error message,
I didn't find anything.

I read this section:
http://adam.chlipala.net/cpdt/html/InductiveTypes.html#lab32
Certified Programming with Dependent Types > Introducing Inductive Types  >
Nested Inductive Types

coq accepted the proof now.
Thanks!

- -- 
$_="sccc,gB1,a_oo,JosBackuSa,g11,ug1a,oscc,cBBg,JcgaBuucaB_s11_Juc_c";
while(($c,$b,$a)=m/^(.)([^,]*),(.*)$/){$_=$a;s/$c/$b/g;}
print map chr length,split /_/;
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk+5P5oACgkQxzVgPqtIcftymACdFWMSLv4Td3JZSqDJepFU8xWj
8TkAnjb7PBJcqixbJWdCLh4qLCXDM/4q
=HEZ7
-----END PGP SIGNATURE-----