Porting to Coq > 8.4

Hi @barras, I started to port this development to 8.7 which is less easy than I thought. Did you already did some work in this direction, or shall I continue without risking to make twice the same job?

(Initially, I wanted to understand how far we can build the von Neumann hierarchy in pure CIC. We should at least be able to go up to V_ε^CK or are my intuitions wrong?)