Make irrelevant-recompute and corollaries unsafe

[jespercockx]

This is the less invasive alternative to #2998, which instead just makes the definitions that are no longer supported unsafe by putting them in a separate Unsafe module that has the --irrelevant-projections flag.

Currently this is based on the experimental branch, which seems to lag a bit behind on master. I tried to bring it up to date but got a bunch of merge conflicts that I didn't know how to solve immediately. If someone else could bring the experimental branch up to date, I'd be glad to rebase this PR on it.

TODO:

• Merge master into this branch
• Add changelog entry

[jamesmckinna]

I guess we'll only bring experimental up-to-date with master once v2.4 has finally been officially released, but in the meantime, I think that a version of this, even less invasive, can be written directly for merging into master? Specifically, is it not safe to refactor this as

⊥-recompute : Recomputable ⊥
⊥-recompute ()

and hence its corollary ¬-recompute is also safe?