The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 19.03.2013 16:19, schrieb Colm Bhandal:
> Also the equation nth j Nil = Some (Integer n) does
> not hold for Nil. But how to introduce these facts in Coq.

Since nth is defined by recursion on the j, you need to make the 
structure of j visible to Coq before it can reduce it to None. Then use 
discriminate on None = Some ... to close the goal.

This might or might not do the trick:

destruct j ; discriminate.