WyC: continuing to update test cases to use the proper syntax for specifying ensures clauses and type invariants.