Agda: replace some holes with postulates
Agda: replace some holes with postulates

Issue #24 requires splitting up total.agda in different modules.
However, some of the code to move away contains holes, and Agda
rejects importing modules with holes (with an error complaining about
unsolved metas). Hence we need to replace the holes by postulates
before moving the code in another module.

Some of these postulates are clearly wrong and need to be
restricted a bit, so they should be replaced with proofs.

Old-commit-hash: 2012bd3208ab4d269dcab3a436530872e88a8830

inc-lc/ilc-agda