Description
After adjusting the det_ext state as part of #824, a lot of lemmas were fixed to det_ext instead of the more general state_ext class. Some of these are required because they involved functions or properties that operate on the det_ext state, but many were changed just so that we didn't need to think about it, or accidentally as part of a larger crunch.
It would be nice to go through and be more careful about which lemmas are made det_ext, as it will otherwise continue to spread throughout the proofs and be annoying whenever encountered. See https://github.com/corlewis/l4v/blob/1e732c8e3156eff3147ec165293d7aa7b8a66de7/proof/invariant-abstract/DetSchedDomainTime_AI.thy#L31 for an example where all of the lemmas in that locale were fixed to det_ext, even though many didn't need to be.