(VAR n x y xs ys)
(RULES
eq(n,xs,xs) -> T
eq(s(n),c(x, xs),c(x,ys)) -> eq(n, xs, ys)
nats -> c(0, inc(nats))
inc(c(x,xs)) -> c(s(x), inc(xs))
)