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())))
 shuffle(nil()) -> nil()
 shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))

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