Switching to Agda 2.4.0.1.

Because of certain changes in the termination checker, some `with`
constructs have had to be replaced with auxiliary functions.