refactor pool_safe

This MR refactors pool_safe to use a more constructive formulation (see #10).

In short,

• the new definition of pool_safe pushes through the negation at the top of the old definition (which was defined in terms of pool_reach_stuck),
• but leaves the definition of pool_reach_stuck as it is (a definition in terms of pool_safe seems very unconstructive). This is relevant in particular because our definition of behaviour still uses reach_stuck. This definition has the consequence that the equivalence not pool_safe <-> pool_reach_stuck does hold only classically or with decidability of reduction now.
• we need XM at a few different places in the adequacy proof and in the behaviour metatheory and can drop it at others.
• reach_or_stuck has become safe_reach and is defined in terms of pool_safe now,
• IrredUnless has been replaced by SafeImplies, which is defined as safe P e σ -> ϕ, which mostly matches the def we show on paper.

This entails that also the relevant lemmas for exploiting safety have been renamed, e.g.:

• source_red_irred_unless has become source_red_safe_implies,
• safe_reach_irred has become safe_reach_safe,
• pool_safe_irred has become pool_safe_implies.

@jung or @msammler : can you review if you are fine with the naming changes?