<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>