make: `tl.lp' is up to date.

hc> (length nil z)
ll> (bottom o-o bottom)
Invariant proved.

hc> (pi X, L, N. ((length (cons X L) (s N)) <== (length L N)))
ll> (pi X, L, N. (((stroke par L) o-o (stroke par N)) <== (L o-o N)))
Invariant proved.