Remove remaining duplication between abs₁ ... abs₆

This relies on Agda 2.4.0's varying arity in a more essential way.
Pick correct base case for recursive functions

A little duplication remained, because absN and absV do not have as base
case arity 0 but arity 1, just because the case for arity 0 is not very
useful per se. Hence, abs{N,V} need to unroll one recursive invocation
into the base case, and need to have an helper (absNBase) to factor out
the ensuing duplication.

This commit fixes that; next commit will inline absNBase.
Inline absNBase away and normalize resulting code
Tons of cleanups to absN/V

Among others, reverse list of type arguments, so that the final type
signature is the one you'd expect, without exposing implementation
artifacts.