The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Eric Finster wrote:
> Based on Adam's response (thanks Adam!) I came up with the following:
>
>     Fixpoint zero_len_eq (A : Type) n (v : Vect A n) :=
>       match v in (Vect _ n) return (match n with O =>  identity _ _ | S
> _ =>  unit end) with
>         | VNil =>  identity_refl (VNil A)
>         | VCons _ _ _ =>  tt
>       end.
>
> Which looks like some good progress.
>    

I should also have pointed to Section 12.3.4 of CPDT, which should 
definitely clear this up.  In general, I feel anyone who's doing serious 
proving with Coq should read the whole book. ;)