in emptop, generalize the statements slightly, fix the proofs, and rename to cntrcolim