Problem:
 insert n nil (\x y. F x y) (\x y. G x y) -> cons n nil
 insert n (cons h t) (\x y. F x y) (\x y. G x y) ->
   cons (F n h) (insert (G n h) t (\x y. F x y) (\x y. G x y))
 sort nil (\x y. F x y) (\x y. G x y) -> nil
 sort (cons h t) (\x y. F x y) (\x y. G x y) ->
   insert h (sort t (\x y. F x y) (\x y. G x y)) (\x y. F x y) (\x y. G x y)
 asort l -> sort l (\x y. min x y) (\x y. max x y)
 dsort l -> sort l (\x y. max x y) (\x y. min x y)

Proof:
 Higher-Order Church Rosser Processor:
  insert n nil (\x y. F x y) (\x y. G x y) -> cons n nil
  insert n (cons h t) (\x y. F x y) (\x y. G x y) ->
    cons (F n h) (insert (G n h) t (\x y. F x y) (\x y. G x y))
  sort nil (\x y. F x y) (\x y. G x y) -> nil
  sort (cons h t) (\x y. F x y) (\x y. G x y) ->
    insert h (sort t (\x y. F x y) (\x y. G x y)) (\x y. F x y) (\x y. G x y)
  asort l -> sort l (\x y. min x y) (\x y. max x y)
  dsort l -> sort l (\x y. max x y) (\x y. min x y)
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed