The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

I'm having some trouble dealing with dependently-typed functions where 
multiple parameters' types depend on the same other parameter.  I'm 
hoping someone on this list can set me straight.

As a simple example, I am trying to prove a property of the Bvector type 
from the standard Bvector module.  I've defined:

Definition beven : forall n, Bvector n -> bool := (* code elided *).
Definition band32 := BVand 32.

beven checks if the natural number interpretation of a bit vector is 
even, and band32 implements bitwise AND on 32-bit vectors.  While 
constructing a proof, I end up with this goal:

  e1 : Bvector 32
  e2 : Bvector 32
  ============================
   (beven e1 || beven e2) = beven (band32 e1 e2)

I want to perform case analysis on e1 and e2, which should make the 
proof easy, since the truth of the goal formula only depends on the 
first bit of each.  However, if I try:

destruct e1.

I get the error:

User error: Cannot solve a second-order unification problem

Can anyone suggest how I might go about proving this goal?

Thanks!