Q. Page 2 of the 3-25 notes says
        length(x)    &=& length(tail(x))  (provided x =/= [ ])
     Is that correct?

A. No, that is not correct.  It should be

        length(x)    &=& 1 + length(tail(x))  (provided x =/= [ ])