2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/229307We prove in this paper that the types of system F inhabited uniquely by ?I-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.Logictext