Problem:
 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))

Proof:
 Open