let rec merge ((x, y, _) as e) s =            
  assert (Fact.Equal.both_sides (is_canonical s) e);
  if not(Term.eq x y) then
    begin 
      Trace.msg "v" "Union" e Fact.Equal.pp;
      union s e
    end 




(** Merging x = y is performed by adding x |-> y and eager path compression by replacing all links z |-> x with z |-> y. *)


and union s (x, y, rho) = 
  assert(not(Term.eq x y));            (* [rho |- x = y] *)
  let removable' = 
    if !garbage_collection_enabled &&
      Term.Var.is_internal x 
    then 
      Term.Var.Set.add x s.removable
    else 
      s.removable
  in 
  let pre_of_x = inv s x in 
  let post' = 
    Pre.fold
      (fun z ->                         (* [tau |- z = x] *)
         let (_, tau) = find s z in
         let sigma = Jst.dep2 tau rho in
           Term.Var.Map.add z (y, sigma))
      pre_of_x
      (Term.Var.Map.add x (y, rho) s.post)
  in
  let pre' = 
    try
      let pre_of_y = pre s y in
      let pre_of_y' = Pre.add x (Pre.union pre_of_y pre_of_x) in
        Term.Var.Map.add y pre_of_y'
          (Term.Var.Map.remove x s.pre)
    with
        Not_found -> 
          Term.Var.Map.add y (Pre.add x (inv s x))
          (Term.Var.Map.remove x s.pre)
  in
  let cnstrnt' =
    try
      let (cx, tau) = cnstrnt s x in
        (try
           let (cy, sigma) = cnstrnt s y in
             if Var.Cnstrnt.sub cy cx then
               Term.Var.Map.remove x s.cnstrnt
             else 
               (try
                  let c = Var.Cnstrnt.inter cx cy  in
                    Term.Var.Map.add y (c, Jst.dep3 rho tau sigma) 
                      (Term.Var.Map.remove x s.cnstrnt)
                with
                    Var.Cnstrnt.Empty -> 
                      raise(Jst.Inconsistent(Jst.dep3 rho tau sigma)))   
         with
             Not_found -> 
               Term.Var.Map.add y (cx, Jst.dep2 rho tau) 
                    (Term.Var.Map.remove x s.cnstrnt))
    with
        Not_found -> s.cnstrnt
  in
    s.post <- post'; 
    s.pre <- pre'; 
    s.cnstrnt <- cnstrnt';
    s.removable <- removable'