got up to algebra1b with coq 8.4

But I'm now working from a patched version of coq 8.4 that implements
type in type and relevance of inductive index levels, available here:

   https://github.com/DanGrayson/coq/commit/c7a19becc2e286bc878e592f6ad133642c2f36a6