let rec cmp a b = 
  match a, b with  
    | Var(x, _), Var(y, _) -> Var.cmp x y
    | Var _, App _ -> 1
    | App _, Var _ -> -1
    | App(f, l, _), App(g, m, _) ->
        (match l, m with
           | [], [] -> 
               Sym.cmp f g
           | [], _ -> -1
           | _, [] -> 1
           | [x], [y] -> 
               let c1 = Sym.cmp f g in 
                 if c1 <> 0 then c1 else cmp x y
           | [_], _ -> -1
           | _, [_] -> 1
           | [x1; x2], [y1; y2] ->
               let c1 = Sym.cmp f g in 
                 if c1 <> 0 then c1 else
                   let c2 = cmp x1 y1 in
                     if c2 <> 0 then c2 else cmp x2 y2
           | [_; _], _ -> -1
           | _, [_; _] -> 1
           | _ ->
               let c1 = Sym.cmp f g in
                 if c1 != 0 then c1 else cmpl l m)
 
and cmpl l m =
  let rec loop c l m =
    match l, m with
      | [], [] -> c
      | [], _  -> -1
      | _,  [] -> 1
      | x :: xl, y :: yl -> 
          if c != 0 then 
            loop c xl yl 
          else 
            loop (cmp x y) xl yl
  in
  loop 0 l m