<div dir="ltr">You use the List for its strucutre/spine effectively only, so it can be reduced to a Nat instead at least.<br><br>Upon a further look, as far as I can tell, your function makeLevels returns (a , b) if the list is empty, and (a âŠ” b , a âŠ” b) otherwise:<br><br>n = 0:<br>makeLevels [] = a , b<br>done<br><br>n = 1:<br>makeLevels (x :: []) =><br>let (c , d) = makeLevels [] in (c âŠ” d , c âŠ” d) =><br>(a âŠ” b , a âŠ” b)<br>done<br><br>n = n' + 2:<br><br>makeLevels (x :: xs) = <br>let (c , d) = makeLevels xs in (c âŠ” d , c âŠ” d) => // by ih c = a âŠ” b and d = a âŠ” b<br>((a âŠ” b) âŠ” (a âŠ” b) , (a âŠ” b) âŠ” (a âŠ” b)) <br><br>This is the only part I'm not sure about - is âŠ” commutative and associative, and is x âŠ” x == x? (And of course, does agda solve these equations "under the hood"?)<br><br>If they are, then my argument should hold.</div>