Problem:
 foldl (\x y. F x y) n nil -> n
 foldl (\x y. F x y) n (cons h t) -> foldl (\x y. F x y) (F n h) t
 sum l -> foldl (\x y. plus x y) 0 l

Proof:
 Higher-Order Church Rosser Processor:
  foldl (\x y. F x y) n nil -> n
  foldl (\x y. F x y) n (cons h t) -> foldl (\x y. F x y) (F n h) t
  sum l -> foldl (\x y. plus x y) 0 l
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed