Assertions in the runtime library for obvious preconditions and proof obligations

[bandurvp]

The Continental model revealed that

• proof obligations are not discharged in a standard modelling activity such as theirs
• simple assertions for the obvious cases of non-existent keys, heads of empty lists etc. in the runtime library would be extremely useful

In this issue we should add support for obvious proof obligations and preconditions in the runtime library. The preferred assert statement is assert(condition && message_text). @peterwvj this is my responsibility, but any thoughts otherwise?

[peterwvj]

I'm OK with adding those checks. It's similar to the assertions we've already added to ensure that the TVPs passed to certain functions carry the right types (e.g. the runtime version of + expects numbers).

[bandurvp]

Yeah, that's the kind of check that's missing in some parts of the runtime. I'll add those now.