The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi,

Sorry to bother the list again, but I've been reading the manual and 
can't find any explanation of this error message:

User error: Cannot solve a second-order unification problem.

I get this error when attempting to prove the following theorem:

Inductive bits : nat -> Set :=
    | Bnil : bits 0
    | Bcons : forall n:nat, bool -> bits n -> bits (S n).

Theorem only_one_bits0 : forall (bs:bits 0), bs = Bnil.
Proof.
intro bs.
case bs. (* fails *)

It seems clear to me that a value of type "bits 0" has to be Bnil, as 
the other constructor has type "bits (S n)", but I can't figure out how 
to express this. Any help would be greatly appreciated.

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com