let add d s = 
  assert(Fact.Diseq.is_var d);
  assert(closed s);
  let (x, y, rho) = d in    (* [rho |- x <> y] *)
    match is_diseq s x y with
      | Some _ -> 
          (s, Fact.Diseq.Set.empty)
      | None ->
          Trace.msg "d" "Add(d)" d Fact.Diseq.pp;
          let dx' = Set.add (y, rho) (diseqs s x)
          and dy' = Set.add (x, rho) (diseqs s y) in
          let s' = 
            Term.Map.add x dx'
              (Term.Map.add y dy' s)
          in
            assert(closed s');
            (s', Fact.Diseq.Set.singleton d)