let restrict a s =
  try
    let (i, _) = apply s a in
      Trace.msg "c" "Restrict" a Term.pp;
      changed := Term.Set.remove a !changed;
      Term.Map.remove a s
  with
      Not_found -> s