prove zHEAP_UPDATE_REF

not sure it's right though: haven't updated the bytecode simulation
theoerm yet.