Problem:
 eq(0(),0()) -> true()
 eq(s(X),s(Y)) -> eq(X,Y)
 eq(X,Y) -> false()
 inf(X) -> cons(X,inf(s(X)))
 take(0(),X) -> nil()
 take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
 length(nil()) -> 0()
 length(cons(X,L)) -> s(length(L))

Proof:
 Containment Processor: loop length: 1
                        terms:
                         inf(X)
                        context: cons(X,[])
                        substitution:
                         X -> s(X)
  Qed