let diseqs p x =
  let (y, rho) = find p x in                   (* [rho |- x = y] *)
  let ds = D.diseqs p.d y in
    if Term.eq x y then ds else
      D.Set.fold 
        (fun (z, tau) ->                       (* [tau |- y <> z] *)
           let sigma = Jst.dep2 tau rho in
             D.Set.add (z, sigma))
        ds D.Set.empty