Fix examples/parsing/NTproperties in light of 932238d

Issue in latter commit is its introduction of theorem FLAT_EQ_NIL,
which overrode my own local theorem of the same name. Fixing the order
of the open declarations fixes this, but I also simplified a couple of
proofs slightly along the way.
Use [simp] rather than export_rewrites in a few places.