BVP work on live-var annotation optimiser
pLive: Handle case corrected and proved
pLive: Assign case proved
pLive: If case proved
minor tweak to BVP semantics of tail calls
BVP better stack lemmas: stack can be swapped
pLive: Call case proved