I just prove erasure for heap_lang prophecies. This still needs (serious) cleanups. Any feedback is welcome.
heap_lang