(VAR X N L IL M)
(RULES 
zeros -> cons(0)
and(tt) -> X
length(nil) -> 0
length(cons(N)) -> s(length(L))
take(0,IL) -> nil
take(s(M),cons(N)) -> cons(N)
)