Improve TreeMap Heaps

[markusdemedeiros]

TreeMap heaps currently do not support allocation. Instanstate UnboundedHeap for them in HeapInstances.lean.

The challenge in this is going from a TreeMap (which has finite domain) to a key that does not exist in the map. If you can do this, it becomes your fresh function. Like the AssocList heap, your NotFull predicate should be True.

[MackieLoeffel]

Finding a fresh key should be possible using the maxKey function: https://leanprover-community.github.io/mathlib4_docs/Std/Data/ExtTreeMap/Basic.html#Std.ExtTreeMap.maxKey

(via #iris-lean > stdpp @ 💬 )