Somewhat miraculously, minor surgical changes to one of the proofs
were all it took to make CancelTacBedrock work with no-Const.
I don't fully understand why the changes I made were necessary.
I also have no idea if the tactic actually works.