let is_diseq s x y =
  try
    Set.iter
      (fun (z, rho) ->
         if Term.eq y z then
           raise(Found(rho)))
      (diseqs s x);
    None
  with
      Found(rho) -> Some(rho)