(VAR f h l l1 l2 l3 t )
(RULES 
        app(app(append,nil),l) -> l
        app(app(append,app(app(cons,h),t)),l) -> app(app(cons,h),app(app(append,t),l))
        app(app(map,f),nil) -> nil
        app(app(map,f),app(app(cons,h),t)) -> app(app(cons,app(f,h)),app(app(map,f),t))
        app(app(append,app(app(append,l1),l2)),l3) -> app(app(append,l1),app(app(append,l2),l3))
        app(app(map,f),app(app(append,l1),l2)) -> app(app(append,app(app(map,f),l1)),app(app(map,f),l2))
        
)