Hi all, I need an impredicative Prop universe. Would it be lot of work to add an experimental "--impredicative-prop" flag? I am also aware of this hack of Martin Escardo: http://www.cs.bham.ac.uk/~mhe/impredicativity/ But I am not sure to which extent I can adapt it to my needs... Cheers, Simon