Did most of HoareAsLogic

Right now the very last clause of the very last proof has me stumped.
I'll come back to it in a few days, see what I can do then.