This MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still called checked_closed).