let merge e s = 
  Trace.msg "d" "Merge" e Fact.pp_equal;
  let (a, b, _) = Fact.d_equal e in
  let da = deq s a and db = deq s b in
  if Term.Set.mem a db || Term.Set.mem b da then
    raise Exc.Inconsistent
  else
    let dab = Term.Set.union da db in
    if db == dab then
      (Term.Set.empty, Term.Map.remove a s)
    else
      let ch' = Term.Set.singleton b in
      let s' = Term.Map.add b dab (Term.Map.remove a s) in
        (ch', s')