Introduce intermediate monad interfaces in the shallow/symbolic executors

[skeuchel]

Both the shallow and the symbolic executors are implemented in a continuation monad with a proposition answer type. Sometimes we break this abstraction. To fix this I propose to define a type class interface that gathers the essential operations for both the symbolic and shallow executors and make our current monad an instance of it. The soundness proof of the symbolic executor would then take two related instances etc..

This would also allow us to more easily experiment with other implementations, like for instance a codensity-transformed free monad, which would allow us to generate subtrees only, i.e. for experiments with state-merging etc.