Changes

Summary

1. Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.
2. proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
3. unused (see fe9e590ae52f);
4. clarified modules;