 NFP (predicative NF), the version of NF in which one accepts only instances of the axiom of comprehension which can be typed so as to be instances of comprehension of predicative TST (described above under type theories) was shown to be consistent by Marcel Crabbé (1982). He also demonstrated the consistency of the theory NFI in which one allows all instances of stratified comprehension in which no variable appears of type higher than that assigned to the set being defined (bound variables of the same type as that of the set being defined are permitted, which allows some impredicativity). One would like to read the name NFI as “impredicative NF” but one cannot, as it is more impredicative than NFP, not more impredicative than NF itself.