vc explanations: somehow indicate side conditions?

[Philipp15b]

at the moment, our vc explanations for high-level constructs such as while loops or proc calls just show the invariant/pre as the explanation, but they don't ever show that there are side-conditions. ideally, we'd somehow also show that e.g. I <= Phi(I) must hold, referencing the loop body's pre explanation as part of Phi(I).