Compilation
===========

coqc -R . Top LNMItPred.v;
coqc -R . Top LNGMItPred.v;
coqc -R . Top LamFlatPred.v;
coqc -R . Top -impredicative-set LNMItImp.v;
coqc -R . Top -impredicative-set LNGMItImp.v


Exploration
===========

for the files *Pred.v, use ProofGeneral thanks to the file _CoqProject

for the files *Imp.v, use coqide -impredicative-set *Imp.v