[Agda] [PATCH] add a ∷-injective for Vec like there is one for List

[Helmut Grohne]

Hi,

I found myself in need of injectivity of Vec._∷_ in a few places. While
there is a ∷-injective for List, there is none for Vec yet. I attach a
simple patch (in a format suitable to git am) to address this omission
and license it under the MIT license used for the standard library. I'd
appreciate if it could be merged. Thanks.

Helmut
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-add-a-injective-for-Vec-like-there-is-one-for-List.patch
Type: text/x-patch
Size: 1402 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140117/846f592a/0001-add-a-injective-for-Vec-like-there-is-one-for-List.bin