Signed-off-by: Michael McInerney <[email protected]>

An assert is added in order to provide extra information regarding
liveness for objects in the region to be detyped, in preparation for
forthcoming work that will add fields to the TCB object and modify
the definition of liveness.

The assert is added separately from the current assert in deleteObjects
since these asserts are shown to hold via lemmas which occur in
different locales.

Greater use of the definition schact_is_rct is made in general, and in
particular, in some top-level theorems, but note that the guards and
preconditions of top-level theorems have not been strengthened.

Signed-off-by: Michael McInerney <[email protected]>