Investigate further use of `none_top/none_bot` in the proofs

[michaelmcinerney]

One immediate use is valid_bound_ntfn', which could use the abbreviation opt_tcb_at', which uses none_top.

Others include places where case_option is used, and where case statements are used with option types.