let rec unify = function 
    [] -> [] 
  | (Var x, t):: q  | (t,Var x)::q 
      ->
      if t = Var x then unify q else 
        if 
          List.mem x (vars t) 
        then failwith "unify"
        else 
          let
            q' =
            List.map 
              (function (t1,t2) -> 
                 (apply_subst [(x,t)] t1,apply_subst [(x,t)] t2))
              q
          in
            compsubst  (unify q') [(x,t)]
  | (Operation(f,ff),Operation(g,fg))::q ->
      if( f = g && (List.length ff) = (List.length fg))
      then unify ((List.combine ff fg)@q)
      else failwith "unify"