<div dir="ltr"><div>Hello guys,<br><br></div>I am trying to write a function on indexed types:<br><div><div><a href="https://gist.github.com/dima-starosud/7100947b0e243ea6a034">https://gist.github.com/dima-starosud/7100947b0e243ea6a034</a><br>But I cannot understand the reason of the error messages shown, and how to solve issues arisen.<br></div><div><br></div><div>Please see a gist (link above).<br></div><div>Ideally I wanted &quot;reduce₁&quot;. But that didn&#39;t compile. (And I think I can imagine the reason why)<br><br></div><div>Next attempt was &quot;reduce₂&quot;. But this would involve a lot of unnecessary code on RHSs.<br><br></div><div>Than I decided to improve it and got &quot;reduce₃&quot;, but it gave me completely puzzling error message.<br><br></div><div>Please help me to understand all that stuff Agda communicates to me.<br></div><br></div><div>I would like something really simple (like &quot;reduce₁&quot;), probably with help of <b>pattern</b>s.<br></div><div><br></div><div>Thanks in advance,<br></div><div>Dmytro <br><br></div></div>