Remove lots of duplication across abs₁ .. abs₆

The new code is much more clever. Still not perfect, with varying
arities we can probably do better.
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.
Drop compatibility wrappers

I also verified that type inference is unable to infer the argument
count. I can live with that.
Merge pull request #3 from inc-lc/topic/abstract-abs-smart-constrs

Abstract abs* smart constructors for HOAS