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

[Kenichi Asai]

Hi Andreas,

> 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

I don't think I can do this.  The code is from stackoverflow, and I
don't quite understand all of the code.  We also want to have
heterogeneous versions of other functions, but I don't think I can
write them.  (I actually want to have hcong2 for my project now, but I
am having hard time writing it.)  It would be great someone else can
write them and place a request.  Thanks in advance.

Sincerely,

-- 
Kenichi Asai