Strong monotonicity proofs for the new shallow executor

[skeuchel]

The new shallow executor currently only has weak monotonicity proofs like e.g. https://github.com/katamaran-project/katamaran/blob/1ff10d9e74e66e89ed9f9729dea041f2d488d7dc/theories/Staging/NewShallow/Executor.v#L917-L922

This monotonicity property is not strong enough to finish the soundness proof of the new shallow executor. We loose the (non-persistent) induction hypothesis from the Löb induction when using it https://github.com/katamaran-project/katamaran/blob/1ff10d9e74e66e89ed9f9729dea041f2d488d7dc/theories/Staging/NewShallow/IrisInstance.v#L896-L916

We can probably make this quite structured like the current monotonicity proofs if we build up respectful, forall_relation, pointwise_relation etc. relation constructors up over separation logic propositions. This can probably hugely benefit from https://github.com/katamaran-project/katamaran/issues/36