Def. 4.4: can the final square go at the end of the last line instead
of a line by itself?


Def. 4.13


> s[x′/x]p: substitutes all appearances of a mathematical expression x
> with a math- ematical expression x′ in top(s, p)