let union i e s =  
  let (x, b, j) = Fact.d_equal e in
  assert(is_var x);
  Trace.msg (to_string i) "Update" (x, b) Term.pp_equal;
  if Term.eq x b then 
    s 
  else
    let use' = 
      try 
        Use.remove x (fst(Map.find x s.find)) s.use 
      with 
          Not_found -> s.use 
    in
      {find = Map.add x (b,j) s.find;
       inv = Map.add b x s.inv;
       use = Use.add x b use'}