[Agda] Sized types question

[Deyaaeldeen]

Hi,

I need help to understand why Agda wants the constraint j <= i to hold in
the attached file.

Thanks!

Deyaa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190227/e089f3e4/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Failure.agda
Type: application/octet-stream
Size: 433 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190227/e089f3e4/attachment.obj>