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.
update PLDI14-List-of-Theorems.agda for consistency with #4

Camera-ready version inserts a "lemma 2.5", which means math items
2.5--2.9 should be renumbered 2.6--2.10.

Relevant commits:
23339dd5a9e56c3c31d42252c4020b716ec77725
0c1e97fbf3b62bddf23559545a4c801b4189cb29
Merge pull request #3 from inc-lc/topic/abstract-abs-smart-constrs

Abstract abs* smart constructors for HOAS
require agda-lib-0.8 (v0.7 fails to typecheck under agda 2.4)
Merge remote-tracking branch 'origin/master' into topic/nil-extension

The conflicts were with the refactoring of abs₁ ... abs₆ interface.
After updating new users, the merge result typechecks again.

Conflicts:
	Nehemiah/Change/Term.agda
	Parametric/Change/Term.agda