The Coq mailing list

[Eric Finster <ericfinster AT gmail.com>]

Hi Again,

>>
>> It would be nice to have something like a condensed cheat sheet version
>> of Adam's book...
>>

Yes, that would be great.  Though one wonders if the cheat sheet might
end up the same size as the book ... :)  Ultimately sometimes I guess
it's just quicker to ask, so I appreciate people taking time out to
answer or give pointers.

>
> Lemma vector0_nil:
>  forall (X:Type) (v:vector X 0), v = vector_nil.
> Proof.
> inversion v using @vector0_rect.
> reflexivity.
> Qed.
>

This I think is roughly what I originally had in mind, but having more
than one solution is always a plus!  Thanks everybody.

Eric