This is necessary, but not sufficient: we must implement
cumulative checking at some point.

Cany is short-circuited, to avoid trivially true invariant
preservation VCs for "val x : <mutable type with invariant>".
Still gonna get those for "val ref x : <mutable type w/inv>",
unfortunately, since the right-hand side becames an application.