added a coercion; disabled the type invariant; other minor changes

Note: this also adds some "noise" to schoolbook.mlw, but that might be useful for the moment, so I did decide to add that to the PR.