let rec compare_terms x y =
  if term_equal x y then
    0
  else
    match x, y with
        (* var first *)
      | Var u, Var v ->
          Var.compare u v
            
      | Var _, _ ->
          -1
            
      | _, Var _ ->
          1

      (* const second *)
      | Const a, Const b ->
          Symbol.compare a b
            
      | Const _, _ ->
          -1
            
      | _, Const _ ->
          1
            
      (* function term last *)
      | Func func1, Func func2 ->
          let cmp =
            Symbol.compare func1.symbol func2.symbol
          in
            if cmp <> 0 then
              cmp
            else
              let rec compare_terms' index =
                if index >= Array.length func1.subterms then
                  0
                else
                  let cmp' =
                    compare_terms func1.subterms.(index) func2.subterms.(index)
                  in
                    if cmp' <> 0 then
                      cmp'
                    else
                      compare_terms' (index + 1)
              in
                compare_terms' 0