gen_heap: provide init lemma for non-empty heap that provides the points-to facts
Our current gen_heap_init can be used with a non-empty heap, but then the points-to facts for the initial location are lost. Sometimes however they are needed: both Perennial and time-credits violate the gen_heap abstraction to be able to initialize with a non-empty heap and obtain all the points-to facts.
We should just provide a lemma for this. However, this is blocked on gmap_view having such a lemma, which requires having "map fragments" besides the currently available "singleton fragments".