Formula::NF() now flattens before normalizing.

Formula::Flatten() may introduce new universally quantified variables.
Formula::Normalize() pull universally quantified variables out of K
modalities.
So it makes sense to flatten first.