This makes the proofs a lot nicer. I tried factoring out some properties
about finite maps, but this was not entirely satisfactory. It would be nice
to generalize from_heap_None and heap_singleton_inv_l somehow.