Working

Busy working again.

--
This time I'm (finally) with Agda.

---

Now I'm living with all the mess like this:

--
Not all that bad, actually, since this forces me to think more thoroughly. XD

---

The experience with qsort seems to be quite helpful here.

--
Totally nontrivial...