[Heap.lean](https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/Std/Heap.lean) contains a general interface for heap and map types. Instantiate this for the Heap types in the Lean standard library (eg. [ExtTreeMap](https://leanprover-community.github.io/mathlib4_docs/Std/Data/ExtTreeMap/Lemmas.html)).