[Agda] An exercise in typing

[Roman]

Ulf, that's a cool solution.

I simplified it a little by dropping the second argument from
`forallN`: https://gist.github.com/effectfully/dab7fd1ad7c15d81d386f1aef6632725

(it doesn't really simplify the logic, just the appearance)

If you feel like doing another version of the challenge, it's possible
to solve it by recursing on `n` only once at the term level, rather
than twice in quadratic fashion (you do `mapForallN n` at each
recursive step). Not that it matters though.

Great solution!