[Agda] Re: How can I prove associativity of vectors?

[Helmut Grohne]

On Wed, Dec 17, 2014 at 11:44:28AM +0200, Andreas Abel wrote:
> The hcong' you suggest would be a nice addition to the standard
> library.  Feel free to create a pull request to
> 
>   https://github.com/agda/agda-stdlib

This was suggested earlier, but Ulf Norell was not happy with it. The
corresponding thread starts at:

https://lists.chalmers.se/pipermail/agda/2014/006464.html

If there is consensus now that we do want it, I can submit a git branch
for including it (next year).

Helmut