let dismerge p d =  
  assert(Fact.Diseq.is_var d);
  let d' = Fact.Diseq.map (find p) d in
  let (x', y', rho') = d' in
    if Term.eq x' y' then
      raise(Jst.Inconsistent(rho'))
    else 
      let (d', ds') =  D.add d' p.d in
        p.d <- d'; 
        p.diseq <- Fact.Diseq.Set.union ds' p.diseq