Problem:
 append nil l -> l
 append (cons h t) l -> cons h (append t l)
 append (append k l) m -> append k (append l m)
 map (\x. F x) nil -> nil
 map (\x. F x) (cons h t) -> cons (F h) (map (\x. F x) t)

Proof:
 Higher-Order Church Rosser Processor (kb):
  append nil l -> l
  append (cons h t) l -> cons h (append t l)
  append (append k l) m -> append k (append l m)
  map (\x. F x) nil -> nil
  map (\x. F x) (cons h t) -> cons (F h) (map (\x. F x) t)
  critical peaks: 3, all joinable
   append 196 m <-[0,1]-> append nil (append 196 m)
   append (cons 234 (append 235 236)) m <-[0,1]-> append (cons 234 235) (append 236 m)
   append (append 278 (append 279 280)) m <-[0,1]-> append (append 278 279) (append 280 m)
   
   HORPO Processor:
    precedence:
     map ~ append > cons ~ nil
    problem:
     
    Qed