<div dir="ltr"><div>Hi,</div><div><br></div><div>I need help to understand why Agda wants the constraint j <= i to hold in the attached file.</div><div><br></div><div>Thanks!</div><br clear="all"><div><div dir="rtl" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="rtl"><div style="text-align:left">Deyaa<br></div></div></div></div></div></div></div>