RE: Guarded Impredicativity implementation