Perennial currently has to re-prove gen_heap_init because it needs to know that the inG instances stay the same when turning gen_heapPreG into gen_heapG. This comes from the fact that Perennial needs to instantiate the heap multiple times during an execution to account for crashes: gen_heap_init is called after each crash to pick new ghost name instances.