MAYBE

Problem:
 app(app(mapbt(),f),app(leaf(),x)) -> app(leaf(),app(f,x))
 app(app(mapbt(),f),app(app(app(branch(),x),l),r)) ->
 app(app(app(branch(),app(f,x)),app(app(mapbt(),f),l)),app(app(mapbt(),f),r))

Proof:
 Open