Added a second Formula::Normalize() to Formula::NF().

It seems to be better to first Normalize() before Flatten(), but we can
do another Normalize() afterwards to do some more simplifications
regarding the new variables (pull them out of modal operators).