Problem:
 fst(0(),Z) -> nil()
 fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z))
 from(X) -> cons(X,from(s(X)))
 add(0(),X) -> X
 add(s(X),Y) -> s(add(X,Y))
 len(nil()) -> 0()
 len(cons(X,Z)) -> s(len(Z))

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