Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again

This does not fully build yet, but make tests/heapprop_nopers.vo works -- so it is good enough for some early feedback from @robbertkrebbers to ensure that I am generally on the right track here. :)