Problem:
 app(app(f,0()),n) -> app(app(hd(),app(app(map(),f),app(app(cons(),0()),nil()))),n)
 app(app(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))

Proof:
 Containment Processor:
  loop length: 1
  terms:
   app(app(f,0()),n)
  context: app(app(hd(),app(app(map(),f),[])),n)
  substitution:
   f -> cons()
   n -> nil()
  Qed