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

[Helmut Grohne]

On Thu, Dec 18, 2014 at 12:33:26AM +0200, Andreas Abel wrote:
> This would mean that the above definition of i-cong can be taken?!

After reading the subthread started by Conor McBride I now realize that
i-cong is indeed a special case of cong₂. To verify this, I went through
all of my code an replaced all uses of i-cong without any problems.
Thus, I believe and agree that i-cong is in fact not needed. I note
however, that when using cong₂, I still had to make a few implicit
parameters explicit to make Agda 2.4.2.2 happy.

Thanks for the explanations!

Helmut