let union x y prf s = 
  Trace.msg "v" "Union" (x, y) Term.pp_equal;
  let invy = 
    Set.add x 
      (try Map.find y s.inv with Not_found -> Set.empty)
  in
    {find = Map.add x (y, prf) s.find;
     inv = Map.add y invy s.inv;
     removable = if is_rename x then Set.add x s.removable else s.removable}