Reading material
Pages 128-131.
Additional material
Question
Is the proof rule
{ Q [ a[e] / v ] } v = a[e]; { Q }
valid?