Open
Description
After adjusting the det_ext state as part of #824, we no longer needed the ekheap and it was removed. To minimise the disruption to existing proofs, the etcbs_of projection and etcb_at predicate were redefined to be on top of kheap (see https://github.com/corlewis/l4v/blob/1e732c8e3156eff3147ec165293d7aa7b8a66de7/proof/invariant-abstract/DetSchedInvs_AI.thy#L39). However, while it seems reasonable to keep a version of etcbs_of, etcb_at is equivalent to tcb_at and should be removed.
The rt branch has had the same changes made to the det_ext state and etcbs_of and etcb_at, so if this is done it should be done on both branches for consistency.