let rec cmp a b =
match a, b with
| Var _, App _ -> 1
| App _, Var _ -> -1
| Var(x), Var(y) -> Var.cmp x y
| App(f, l), App(g, m) ->
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