  NNIL-formulas, introduced by Visser in 1983-1984 in a study of
$\Sigma_1$-subsitutions in Heyting Arithmetic, are intuitionistic propositional
formulas that does not allow nesting of implication to the left. The first
results about these formulas were obtained in a paper of 1995 by Visser et al.
In particular, it was shown that NNIL-formulas are exactly the formulas
preserved under taking submodels of Kripke models. Recently Bezhanishvili and
de Jongh observed that NNIL-formulas are also reflected by color-preserving
monotonic maps of Kripke models. In the present paper, we first show how this
observation leads to the conclusion that NNIL-formulas are preserved by
arbitrary substructures not necessarily satisfying the topo-subframe condition.
Then we apply it to construct universal models for NNIL. It follows from the
properties of these universal models that NNIL-formulas are also exactly the
formulas that are reflected by color-preserving monotonic maps. By using the
method developed in constructing the universal models, we give a new direct
proof that the logics axiomatized by NNIL-axioms have the finite model
property.
