More progress on things.  Also, more frustrations.  I suppose the Big
Open Question is whether asking coq to assume cellTopCell also allows
him to "interpret type theory". (I'm still thoroughly convinced that
cellClosure is absolutely uncontroversial. It really only wants a fancier
version of nCk_assoc)

Signed-off-by: jcmckeown <jesse@sockwright>