WyC: added an implicit assumption after an assertion so that Code.Asserts don't need to be assumed during verification condition generation.  See #377