[Agda] Unification failure when using Pointwise-length

[Deyaaeldeen]

Hello,

I want to use the fact that two lists have the same length if they are
Pointwise, witnessed by the Pointwise-length function. However, Agda
complains about the constructor refl at line 51 in the
self-contained agda file located here:
https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51

Your input is much appreciated.

Deyaa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190107/799e6e8e/attachment.html>