t atPos p returns the subterm of term t at position p.
The standard notation for t atPos p is t|_p.
atPos accounts for AC symbols by interpreting n-ary operator
applications *[t1,t2,..tk-1,tk] as binary applications
t replacePos (s,p) returns the term t' where the subterm at position p
is replaced by s. The standard notation for t replacePos (s,p) is t[s]_p.
replacePos accounts for AC symbols in the same ways as atPos.
FIXME: The AC can be optimized.