The Coq mailing list

[Dimitri Hendriks <Dimitri.Hendriks AT phil.uu.nl>]

Hi,

>From the following definition

Variable A : Set.

Inductive listn : nat->Set :=
  niln  : (listn O)
| consn : (n:nat)A->(listn n)->(listn (S n)).

one might expect (listn O) to be inhabited by niln only.
In other words (l:(listn O)) l = niln, but how to prove it?
Case analysis on l:(listn O) is not permitted
("Cannot solve a second-order unification problem").

Similarly, I need something like:

(n:nat;l:(listn (S n)))(EX a:A | (EX l':(listn n) | l = (consn n a l')))

Is it provable?

Best regards,
Dimitri