let merge e s =
  Trace.msg "d" "Merge(d)" e Fact.Equal.pp;
  assert(Fact.Equal.is_var e);
  assert(closed s);
  let x, y, rho = e in           (* [rho |- x = y] *)
    if Term.eq x y then 
      (s, Fact.Diseq.Set.empty)
    else
      match is_diseq s x y with
        | Some(tau) ->           (* [tau |- x <> y] *)
            raise(Jst.Inconsistent(Jst.dep2 rho tau))
        | None -> 
            let fresh = ref Fact.Diseq.Set.empty in
            (try
               let dx = Term.Map.find x s
               and dy = diseqs s y in
                 assert(not(mem x dy));
                 assert(not(mem y dx));
                 let dx' = 
                   Set.fold 
                     (fun (z, tau) ->                       (* [tau |- x <> z] *)
                        let sigma = Jst.dep2 tau rho in     (* ==> [sigma |- y <> z]. *)
                          fresh := Fact.Diseq.Set.add (Fact.Diseq.make y z sigma) !fresh;
                          Set.add (z, sigma))
                     dx Set.empty
                 in
                 let (s', dy') = 
                   (Term.Map.remove x s, Set.union dx' dy)   (* [dx] has to incorporate the new equality! *)
                 in
                 let (s'', dy'') = 
                   Set.fold
                     (fun (z, tau) (s, dy) ->                  (* [tau |- z <> x] *)
                        let dz = diseqs s z in
                          try
                            let dz' = Set.remove (assoc x dz) dz in
                              assert(not(mem x dz'));
                              let sigma = Jst.dep2 tau rho in  (* [sigma|- z <> y] *)
                              let dz'' = Set.add (y, sigma) dz' in 
                              let dy' = Set.add (z, sigma) dy in
                                fresh := Fact.Diseq.Set.add (Fact.Diseq.make y z sigma) !fresh;
                                (Term.Map.add z dz'' s, dy')
                          with
                              Not_found -> (s, dy))
                     dx
                     (s', dy')
                 in
                 let s''' = 
                   if dy'' == dy then s'' else
                     Term.Map.add y dy'' s''
                 in
                   assert(closed s''');
                   assert(not(occurs s''' x));
                   (s''', !fresh)
             with      
                 Not_found -> 
                   assert(not(occurs s x));
                   (s, !fresh))