The Coq mailing list

[roconnor AT theorem.ca]

> > Do you too run into universe inconsistencies?
>
> I did.

I haven't been following your discussion carefully, but I want to point 
you to the previous thread on this topic for your interest

<http://pauillac.inria.fr/pipermail/coq-club/2005/001726.html>

and in particular Gonthier's reply 
<http://pauillac.inria.fr/pipermail/coq-club/2005/001743.html>

which lead to the developement on the coq wiki at
<http://cocorico.cs.ru.nl/coqwiki/UntypedLambdaTerms> (see Non-uniform De 
Bruijn Indices)

and instigated the changes to coq to allow nested datatypes 
parametrically.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''