Deprecate existing definition of ⊥-elim in favour of its irrelevant version ⊥-elim-irr

[jamesmckinna]

          I further conjecture on #2329 that all uses of `⊥-elim` can be replaced by their irrelevant version `⊥-elim-irr`... so question for the maintainers, are we prepared to embrace such a (breaking?) change to the type of `⊥-elim`?

Originally posted by @jamesmckinna in #2243 (comment)

This v3.0 issue concerns the breaking change not undertaken as part of #2243 .

With it, among other things, might go the unification (also breaking) of the types of contradiction and contradiction-irr in Relation.Nullary.Negation.Core and a more systematic treatment of 'computational irrelevance of negated propositions'... considered in #2199.