Vcgen fixes

1) The new vc generator now accepts literals (integers, strings, characters)
2) Reorganization of the proof rules
3) True goals don't show up