Compile with Coq V8.4 (tested with 8.4pl1 of December 2012) coqc LNMItPred.v EFlatCoqPred.v BushPred.v coqc -impredicative-set LNMItImp.v EFlatCoqImp.v BushImp.v LNMItImp.v makes use of an axiom, namely proof irrelevance. EFlatCoqPred.v is axiomatic in the sense that it provides a functor whose argument is a presupposed implementation of LNMIt for LamE. BushPred.v is axiomatic in an analogous way, with a presupposed implementation of LNMIt for Bush. EFlatCoqImp.v and BushImp.v use the implementation given by LNMItImp.v. EFlatCoqImp.v presents esubst in addition to EFlatCoqPred.v, while BushImp.v does not present any new material with respect to BushPred.v (other than showing the benefits of convertibility).