To simplify tail(t):
Simplify t, yielding result x.
Check that x is a list of the form cons(a, b). If not, it is an error.
The simplified form of tail(t) is b.