Problem:
 app(nil(),xs) -> nil()
 app(cons(x,xs),ys) -> cons(x,app(xs,ys))
 rev(nil()) -> nil()
 rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))

Proof:
 Containment Processor:
  loop length: 1
  terms:
   rev(cons(x,xs))
  context: append(xs,[])
  substitution:
   xs -> nil()
   x -> x
  Qed