<div dir="ltr"><div dir="ltr"><div>Hello,</div><div><br></div><div>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</div><div>self-contained agda file located here:</div><div><a href="https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51">https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51</a><br></div><div><br></div><div>Your input is much appreciated.</div><br clear="all"><div><div dir="rtl" class="gmail_signature"><div dir="ltr"><div><div dir="rtl"><div style="text-align:left">Deyaa<br></div></div></div></div></div></div></div></div>