Support "check" mode for hybrid systems

[schillic]

Findings:

• The "check" mode is not as efficient as for purely continuous systems because we still need to compute the flowpipe. However, this can be done lazily. The discrete-post operator will need to handle lazy sets as input, but in theory that is not a problem. Let us see what practice has to say.
• The existing reach_blocks! implementation can be used as follows:
  • Lazy flowpipes: see #479.
  • The property can be passed together with the invariant. There are several ways to go, but all require some refactoring. My current favorite is to model the invariant as a property (for which we maybe need to add an appropriate type). Then we can combine invariant and safety property via a Conjunction from #474.

Observe that this effectively makes the property-checking mode redundant, so it would save a lot of code duplication!