I tried to use sub-expressions in proofs (in a similar way, as in the Paxos proof), but for me it looks like it should be quite fragile, if paths would become longer than a few levels.
It becomes not obvious how to fix a broken path to a sub-expression after the spec itself is modified. Often it is hard to guess, which expression was referred before the modification of the spec.
And they are actually hard to read, again, if they are longer than a few levels. You need to jump between the proof and the formula itself.
But that's just my impression.
Karolis